A compositional automata-based semantics and preserving transformation rules for testing property patterns
Gespeichert in:
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)
Online Zugang:
| 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 | ||