ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 25/3 - 2006  - pp.343-370  - doi:10.3166/tsi.25.343-370
TITRE
Vérification formelle des systèmes temps-réel avec ordonnancement préemptif

RÉSUMÉ
Dans cet article, nous proposons une méthode de vérification de propriétés temporelles quantitatives pour les systèmes temps-réel avec ordonnancement préemptif : le système, modélisé sous la forme d'un réseau de Petri T-temporel étendu à l'ordonnancement, est d'abord traduit en un automate à chronomètres qui lui est temporellement bisimilaire. Puis, la vérification de propriétés temporelles quantitatives est réalisée à l'aide d'H Y T E C H. L'efficacité de cette approche s'appuie sur deux points forts : premièrement, la traduction met en oeuvre une minimisation du nombre de chronomètres de l'automate résultat, ce qui est un paramètre critique pour l'efficacité de la vérification qui s'ensuit. Deuxièmement, la traduction est effectuée par un algorithme surapproximant, à base de Difference Bound Matrix, donc efficace, mais qui produit tout de même un automate temporellement bisimilaire. La méthode a été implémentée et nous fournissons des résultats expérimentaux illustrant son efficacité.


ABSTRACT
In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive scheduling policy: the system, modeled as scheduling time Petri net, is first translated into a stopwatch automaton to which it is timed bisimilar. Timed properties are then verified using H Y T E C H. The efficiency of this approach relies on two strong points: first, the translation features a minimization of the number of stopwatches of the resulting automaton, which is a critical parameter for the efficiency of the ensuing verification. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore efficient, but yields nonetheless a timed bisimilar automaton. We have implemented the method and we give some experimental results illustrating its efficiency.


AUTEUR(S)
Didier LIME, Olivier H. ROUX

MOTS-CLÉS
réseaux de Petri temporels, ordonnancement préemptif, temps-réel, vérification.

KEYWORDS
réseaux de Petri temporels, ordonnancement préemptif, temps-réel, vérification.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (382 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier