Model-Generation of a Fictitious Clock Real-Time Logic Using Sharing Trees

Laurent Ferier, Jean-Francois Raskin, Pierre-Yves Schobbens

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

Current approaches for analyzing timed systems are based on an explicit enumeration of the discrete states and thus these techniques are only capable of analyzing systems with a handful of timers and a few thousand states. We address this limitation by describing how to analyze a timed system fully symbolically, i.e., by representing sets of discrete states and their associated timing information implicitly. We demonstrate the efficiency of the symbolic technique by computing the set of reachable states for a non-trivial timed system and compare the results with the state-of-the-art tools Kronos and Uppaal. With an implementation based on difference decision diagrams, the runtimes are several orders of magnitudes better. The key operation in obtaining these results is the ability to advance time symbolically. We show how to do this efficiently by essentially quantifying out a special variable z which is used to represent the constant zero. The symbolic manipulations given in this paper are sufficient to verify TCTL-formulae fully symbolically.
langue originaleAnglais
titreSMC'99
Sous-titreFirst International Workshop on Symbolic Model Checking
rédacteurs en chefA Cimatti, O Grumberg
Lieu de publicationTrento
EditeurElsevier
Pages107-127
Nombre de pages21
Volume23-1
Etat de la publicationPublié - 1999

Empreinte digitale Examiner les sujets de recherche de « Model-Generation of a Fictitious Clock Real-Time Logic Using Sharing Trees ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation