Dans cet article, nous nous intéressons aux propriétés de disponibilité et à la prévention des dénis de service. Nous proposons un langage d'aspects dédié permettant de prévenir les dénis de service liés à la gestion des ressources. Nos aspects spécifient des politiques de disponibilité en imposant des limites de temps d'allocation des ressources. Dans notre langage, un aspect peut être vu comme une propriété temporelle sur les traces d'exécution. Les programmes et les aspects sont modélisés par des automates temporisés et le tissage par un produit d'automates. L'avantage de cette approche formelle est double : d'une part, l'utilisateur garde la maîtrise de l'impact sémantique du tissage et, d'autre part, il peut utiliser des outils de modelchecking pour optimiser le tissage et vérifier des propriétés de disponibilité.