%0 Journal Article 
%F FHTH06-LOBJET
%A Fradet, Pascal
%A Hong Tuan Ha, Stéphane
%T Systèmes de gestion de ressources et aspects de disponibilité
%J L'Objet - Logiciel, bases de données, réseaux
%V 	 12
%N 2
%P 183-210
%I Hermès/Lavoisier
%X In this paper, we focus on availability properties and the prevention of denial of services. We propose a domain-specific aspect language to prevent the denials of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, an aspect can be seen as a formal temporal property on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties
%8 September
%D 2006
%K Resource management
%K  availability
%K  aspect
%K  weaving
%K  verification
%K  denial of service