caa a22 4500 605516324 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150701xx s 000 0 eng 10.1007/s00165-014-0328-5 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0328-5 A compositional automata-based semantics and preserving transformation rules for testing property patterns [Elektronische Daten] [Safouan Taha, Jacques Julliand, Frédéric Dadeau, Kalou Castillos, Bilal Kanso] Dwyer etal. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal logics (linear temporal logic, CTL, etc.). This translational semantics suffers from two main issues. It is not easily extensible to other patterns or scopes, and it is not always faithful to the natural semantics. In this article, we propose a compositional automata-based approach defining the semantics of each pattern and each scope by an automaton, after which the semantics is composed. Hence, the semantics is compositional and the language is easily extensible. We compare the two semantics by model checking. In some cases, our semantics reveals a lack of homogeneity within Dwyer etal.'s semantics. Finally, we apply this approach in the context of property-based testing, in order to evaluate the quality of a test suite, by measuring the coverage of the property automaton. To allow the tester to adapt the coverage criteria to its goals, we propose transformation rules over the patterns automata that implement relevant unfolding strategies for loops, or predicates labeling the automata transitions. We illustrate these principles by means of an industrial case study. British Computer Society, 2014 Formal methods nationallicence Temporal properties nationallicence Compositional automata semantics nationallicence Temporal logics nationallicence Property patterns nationallicence Testing transformation nationallicence Taha Safouan Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France aut Julliand Jacques FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut Dadeau Frédéric FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut Castillos Kalou FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut Kanso Bilal Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France aut Formal Aspects of Computing Springer London 27/4(2015-07-01), 641-664 0934-5043 27:4<641 2015 27 165 https://doi.org/10.1007/s00165-014-0328-5 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0328-5 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Taha Safouan Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France aut NATIONALLICENCE 700 1- Julliand Jacques FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut NATIONALLICENCE 700 1- Dadeau Frédéric FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut NATIONALLICENCE 700 1- Castillos Kalou FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France aut NATIONALLICENCE 700 1- Kanso Bilal Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/4(2015-07-01), 641-664 0934-5043 27:4<641 2015 27 165