François Taïani, Mario Paludetto, Jérome Delatour, and Thierry Cros

Vérification d'objets temps réel à l'aide des réseaux de Petri et de la logique linéaire

Proceedings of the 9th Conference on Real-time and Embedded Systems (RTS'2001), ISBN:2-87717-078-0, Paris (France), 6-8 Mars, pp. 65-77, Teknea, 2001 (13p.)
Abstract
Cet article aborde la validation de systèmes temps réels dans un cadre de conception orientée objet. Plus spécifiquement nous étudions comment certaines contraintes temporelles imposées par un objet sur son environnement (par exemple délai de réponse borné) peuvent être vérifiées. L'étude considère des objets issus de la méthode de conception temps réel UML / PNO qui allie UML (Unified Modeling Language) aux réseaux de Petri. L'idée principale consiste à appliquer une technique de réécriture basée sur la Logique Linéaire de Girard pour calculer sous forme symbolique les durées de scénario induites par la requête d'un objet. Sur des exemples simples, nous montrons en quoi consiste cette approche et discutons de ses points forts et de ses limitations.

complete document

bibtex

[Maison.png]Back to Home
 
Last generated on 8 Dec 2019       francois.taiani@irisa.fr     Valid HTML 4.0!