A Compositional Automata-based Semantics for Property Patterns

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 : vendredi 14 septembre 2018 - 01:02:54

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

313