{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T13:55:12Z","timestamp":1673013312328},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,7,1]],"date-time":"2015-07-01T00:00:00Z","timestamp":1435708800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Dwyer et\u00a0al. 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 et\u00a0al.\u2019s 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.<\/jats:p>","DOI":"10.1007\/s00165-014-0328-5","type":"journal-article","created":{"date-parts":[[2014,12,9]],"date-time":"2014-12-09T07:43:38Z","timestamp":1418111018000},"page":"641-664","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A compositional automata-based semantics and preserving transformation rules for testing property patterns"],"prefix":"10.1145","volume":"27","author":[{"given":"Safouan","family":"Taha","sequence":"first","affiliation":[{"name":"Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[{"name":"FEMTO-ST\/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"additional","affiliation":[{"name":"FEMTO-ST\/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kalou Cabrera","family":"Castillos","sequence":"additional","affiliation":[{"name":"FEMTO-ST\/DISC-INRIA CASSIS Project, 16 route de Gray, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bilal","family":"Kanso","sequence":"additional","affiliation":[{"name":"Computer Science Department, SUPELEC Systems Sciences (E3S), 3 rue Joliot-Curie, 91192, Gif-sur-Yvette Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press New York","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","unstructured":"Bernet J (2012) Tasccc project\u2014deliverable 5.5\u2014report on the industrial use of the tasccc process. http:\/\/lifc.univ-fcomte.fr\/TASCCC"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Cabrera Castillos K Dadeau F Julliand J Kanso B Taha S (2013) A compositional automata-based semantics for property patterns. In: Johnsen EB Petre L (eds) IFM\u201913 10th international conference on integrated formal methods vol 7940 of LNCS. Springer Turku pp 316\u2013330","DOI":"10.1007\/978-3-642-38613-8_22"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Cabrera Castillos K Dadeau F Julliand J Taha S (2011) Measuring test properties coverage for evaluating UML\/OCL model-based tests. In: Wolff B Zaidi F (eds) ICTSS\u201911 23-th IFIP int. conf. on testing software and systems vol 7019 of LNCS. Springer Paris pp 32\u201347","DOI":"10.1007\/978-3-642-24580-0_4"},{"key":"e_1_2_1_2_5_2","unstructured":"Dwyer MB Alavi H Avrunin G Corbett J Dillon L Pasareanu C Specification patterns. http:\/\/patterns.projects.cis.ksu.edu\/. Accessed 15 Sept 2011"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1998) Property specification patterns for finite-state verification. In: FMSP\u201998 second workshop on formal methods in software practice pp 7\u201315","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE\u201999 21st international conference on software engineering pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Dadeau F Castillos KC Ledru Y Triki T Vega G Botella J Taha S (2013) Test generation and evaluation from high-level properties for common criteria evaluations\u2014the tasccc testing tool. In: ICST\u201913 IEEE sixth international conference on software testing verification and validation pp 431\u2013438","DOI":"10.1109\/ICST.2013.60"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A (2013) Manipulating LTL formulas using Spot 1.0. In: ATVA\u201913 11th international symposium on automated technology for verification and analysis vol 8172 of LNCS. Springer Hanoi pp 442\u2013445","DOI":"10.1007\/978-3-319-02444-8_31"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Gastin P Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: Berry G Comon H Finkel A (eds) CAV\u201901 13th international conference computer aided verification vol 2102 of LNCS. Springer Paris pp 53\u201365","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_2_1_2_11_2","unstructured":"Globalplatform card specification 2.2.1. http:\/\/www.globalplatform.org. Jan 2011"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Gerth R Peled D Vardi MY Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: ISPSTV\u201996 fifteenth IFIP WG6.1 international symposium on protocol specification testing and verification XV. Chapman & Hall Ltd London pp 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Gorbovitski M Rothamel T Liu YA Stoller SD (2008) Efficient runtime invariant checking: a framework and case study. In: WODA\u201908 international workshop on dynamic analysis. Held in conjunction with the ACM SIGSOFT international symposium on software testing and analysis (ISSTA\u201908). ACM New York pp 43\u201349","DOI":"10.1145\/1401827.1401837"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Graf S Sa\u00efdi H (1996) Verifying invariants using theorem proving. In: Alur R Henzinger T (eds) CAV\u201996 computer aided verification vol 1102 of LNCS. Springer Berlin pp 196\u2013207","DOI":"10.1007\/3-540-61474-5_69"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.62"},{"key":"e_1_2_1_2_16_2","unstructured":"Markey N (2003) Temporal logic with past is exponentially more succinct concurrency column. Bull EATCS 79:122\u2013128"},{"key":"e_1_2_1_2_17_2","unstructured":"Myers GJ (1979) Art of software testing. Wiley New York"},{"key":"e_1_2_1_2_18_2","unstructured":"Rouillard D (2012) Tasccc project\u2014deliverable 5.4\u2014report on the integration of the ate requirements. http:\/\/lifc.univ-fcomte.fr\/TASCCC. Accessed 10 Nov 2013"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_1_2_20_2","unstructured":"Taha S OCL temporal extension. http:\/\/www.di.supelec.fr\/taha\/temporalocl\/. Accessed 7 Aug 2012"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Tsay YK et\u00a0al Graphical tool for omega-automata and logics. http:\/\/goal.im.ntu.edu.tw\/wiki\/doku.php. Accessed 24 Oct 2013","DOI":"10.1007\/978-3-642-39799-8_62"},{"key":"e_1_2_1_2_22_2","unstructured":"Utting M Legeard B (2007) Practical model-based testing\u2014a tools approach. Morgan Kaufmann San Francisco"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0328-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0328-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0328-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:15:47Z","timestamp":1641485747000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0328-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,7]]}},"alternative-id":["10.1007\/s00165-014-0328-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0328-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7]]}}}