A compositional automata-based semantics and preserving transformation rules for testing property patterns

Verfasser / Beitragende:
[Safouan Taha, Jacques Julliand, Frédéric Dadeau, Kalou Castillos, Bilal Kanso]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/4(2015-07-01), 641-664
Format:
Artikel (online)
ID: 605516324
LEADER caa a22 4500
001 605516324
003 CHVBK
005 20210128100713.0
007 cr unu---uuuuu
008 210128e20150701xx s 000 0 eng
024 7 0 |a 10.1007/s00165-014-0328-5  |2 doi 
035 |a (NATIONALLICENCE)springer-10.1007/s00165-014-0328-5 
245 0 2 |a A compositional automata-based semantics and preserving transformation rules for testing property patterns  |h [Elektronische Daten]  |c [Safouan Taha, Jacques Julliand, Frédéric Dadeau, Kalou Castillos, Bilal Kanso] 
520 3 |a 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. 
540 |a British Computer Society, 2014 
690 7 |a Formal methods  |2 nationallicence 
690 7 |a Temporal properties  |2 nationallicence 
690 7 |a Compositional automata semantics  |2 nationallicence 
690 7 |a Temporal logics  |2 nationallicence 
690 7 |a Property patterns  |2 nationallicence 
690 7 |a Testing transformation  |2 nationallicence 
700 1 |a Taha  |D Safouan  |u Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France  |4 aut 
700 1 |a Julliand  |D Jacques  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
700 1 |a Dadeau  |D Frédéric  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
700 1 |a Castillos  |D Kalou  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
700 1 |a Kanso  |D Bilal  |u Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France  |4 aut 
773 0 |t Formal Aspects of Computing  |d Springer London  |g 27/4(2015-07-01), 641-664  |x 0934-5043  |q 27:4<641  |1 2015  |2 27  |o 165 
856 4 0 |u https://doi.org/10.1007/s00165-014-0328-5  |q text/html  |z Onlinezugriff via DOI 
898 |a BK010053  |b XK010053  |c XK010000 
900 7 |a Metadata rights reserved  |b Springer special CC-BY-NC licence  |2 nationallicence 
908 |D 1  |a research-article  |2 jats 
949 |B NATIONALLICENCE  |F NATIONALLICENCE  |b NL-springer 
950 |B NATIONALLICENCE  |P 856  |E 40  |u https://doi.org/10.1007/s00165-014-0328-5  |q text/html  |z Onlinezugriff via DOI 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Taha  |D Safouan  |u Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Julliand  |D Jacques  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Dadeau  |D Frédéric  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Castillos  |D Kalou  |u FEMTO-ST/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besançon Cedex, France  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Kanso  |D Bilal  |u Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France  |4 aut 
950 |B NATIONALLICENCE  |P 773  |E 0-  |t Formal Aspects of Computing  |d Springer London  |g 27/4(2015-07-01), 641-664  |x 0934-5043  |q 27:4<641  |1 2015  |2 27  |o 165