Vérification formelle des systèmes temps-réel avec ordonnancement préemptif

摘要

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, mode-Usé sous la forme d'un réseau de Pétri 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'HYTECH. 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 Différence 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é.%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 HYTECH. 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.