A Compositional Automata-based Semantics for Property Patterns

Kalou Cabrera Castillos 1 Frédéric Dadeau 1, 2 Jacques Julliand 1 Safouan Taha 3 Bilal Kanso 3
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 INFO - Département Informatique
E3S - Supélec Sciences des Systèmes [Gif-sur-Yvette]
Abstract : Dwyer et al. define a language to specify dynamic properties based on predefined patterns and scopes. To define a property, the user has to choose a pattern and a scope among a limited number of them. Dwyer et al. define the semantics of these properties by translating each composition of a pattern and a scope into usual temporal logics (LTL, CTL, etc.). First, this translational semantics is not compositional and thus not easily extensible to other patterns/scopes. Second, it is not always faithful to the natural semantics of the informal definitions. In this paper, we propose a compositional automata-based approach defining the semantics of each pattern and each scope by an automaton. Then, we propose a composition operation in such a way that the property semantics is defined by composing the automata. Hence, the semantics is compositional and easily extensible as we show it by handling many extensions to the Dwyer et al.'s language. We compare our compositional semantics with the Dwyer et al.'s translational semantics by checking whether our automata are equivalent to the Büchi automata of the LTL expressions given by Dwyer et al. In some cases, our semantics reveals a lack of homogeneity within Dwyer et al.'s semantics.
Type de document :
Communication dans un congrès
E.B. Johnsen and L. Petre. iFM'2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. Springer, 7940, pp.316-330, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38613-8_22〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00912628
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 2 décembre 2013 - 14:06:05
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, Safouan Taha, Bilal Kanso. A Compositional Automata-based Semantics for Property Patterns. E.B. Johnsen and L. Petre. iFM'2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. Springer, 7940, pp.316-330, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38613-8_22〉. 〈hal-00912628〉

Partager

Métriques

Consultations de la notice

246