Résumé
Cet article s'intéresse au problème de la validation formelle de propriétés temporelles quantitatives et paramétrées pour les systèmes à évènements discrets. Le model checking est une technique d'analyse exhaustive de l'espace des états d'un système modélisé dans un lange formel. Il permet la vérification de propriétés de logique temporelle quantitative. Cependant, l'introduction de paramètres entraine une complexité trop grande de l'analyse, en particulier sur un modèle exprimé en réseaux de Petri temporels. Cet article propose donc une méthode alternative et présente un outil : LPT (Little Parametric Tool) permettant la validation d'une borne temporelle paramétrée. Avec LPT, le modèle du système est analysé et la valeur de la borne maximale est recherchée par l'outil.