Abstractions booléennes pour la vérification des systèmes temps-réel, Tools supported real-time system verification with combination of abstraction/de

Divers
Université

Sous la direction de Stephan Merz Thèse soutenue le 08 novembre 2007: Nancy 1 Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (predicate diagram for timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés. -Model checking This thesis provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finit

Il n'y a aucune évaluation pour l'instant.


Soyez le premier à l'évaluer

Donnez votre évaluation
Abstractions booléennes pour la vérification des systèmes temps-réel, Tools supported real-time system verification with combination of abstraction/de
* Champs obligatoires
Votre commentaire
Vos notes
Clarté du contenu
Utilité du contenu
Qualité du contenu