×

A compositional automata-based semantics and preserving transformation rules for testing property patterns. (English) Zbl 1338.68164


MSC:

68Q55 Semantics in the theory of computing
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

SPOT; LTL2BA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York · Zbl 0915.68015
[2] Bernet J (2012) Tasccc project—deliverable 5.5—report on the industrial use of the tasccc process. http://lifc.univ-fcomte.fr/TASCCC
[3] 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’13, 10th international conference on integrated formal methods, vol 7940 of LNCS. Springer, Turku, pp 316-330 · Zbl 1338.68164
[4] 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’11, 23-th IFIP int. conf. on testing software and systems, vol 7019 of LNCS. Springer, Paris, pp 32-47
[5] Dwyer MB, Alavi H, Avrunin G, Corbett J, Dillon L, Pasareanu C Specification patterns. http://patterns.projects.cis.ksu.edu/. Accessed 15 Sept 2011
[6] Dwyer MB, Avrunin GS, Corbett JC (1998) Property specification patterns for finite-state verification. In: FMSP’98, second workshop on formal methods in software practice, pp 7-15
[7] Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE’99, 21st international conference on software engineering, pp 411-420
[8] 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—the tasccc testing tool. In: ICST’13, IEEE sixth international conference on software testing, verification and validation, pp 431-438
[9] Duret-Lutz A (2013) Manipulating LTL formulas using Spot 1.0. In: ATVA’13, 11th international symposium on automated technology for verification and analysis, vol 8172 of LNCS. Springer, Hanoi, pp 442-445 · Zbl 1410.68223
[10] Gastin P, Oddoux D (2001) Fast LTL to Büchi automata translation. In: Berry G, Comon H, Finkel A (eds) CAV’01, 13th international conference computer aided verification, vol 2102 of LNCS. Springer, Paris, pp 53-65 · Zbl 0991.68044
[11] Globalplatform card specification 2.2.1. http://www.globalplatform.org. Jan 2011
[12] Gerth R, Peled D, Vardi MY, Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: ISPSTV’96, fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification XV. Chapman & Hall Ltd, London, pp 3-18
[13] Gorbovitski M, Rothamel T, Liu YA, Stoller SD (2008) Efficient runtime invariant checking: a framework and case study. In: WODA’08, international workshop on dynamic analysis. Held in conjunction with the ACM SIGSOFT international symposium on software testing and analysis (ISSTA’08). ACM, New York, pp 43-49 · Zbl 0613.03015
[14] Graf S, Saïdi H (1996) Verifying invariants using theorem proving. In: Alur R, Henzinger T (eds) CAV’96, computer aided verification, vol 1102 of LNCS. Springer, Berlin, pp 196-207
[15] Jia Y, Harman M (2011) An analysis and survey of the development of mutation testing. IEEE Trans Soft Eng 37(5): 649-678 · doi:10.1109/TSE.2010.62
[16] Markey N (2003) Temporal logic with past is exponentially more succinct, concurrency column. Bull EATCS 79:122-128 · Zbl 1169.03332
[17] Myers GJ (1979) Art of software testing. Wiley, New York
[18] Rouillard D (2012) Tasccc project—deliverable 5.4—report on the integration of the ate requirements. http://lifc.univ-fcomte.fr/TASCCC. Accessed 10 Nov 2013
[19] Sistla AP, Vardi MY, Wolper P (1987) The complementation problem for Büchi automata with applications to temporal logic. Theor Comput Sci 49(2-3): 217-237 · Zbl 0613.03015 · doi:10.1016/0304-3975(87)90008-9
[20] Taha S OCL temporal extension. http://www.di.supelec.fr/taha/temporalocl/. Accessed 7 Aug 2012
[21] Tsay YK et al Graphical tool for omega-automata and logics. http://goal.im.ntu.edu.tw/wiki/doku.php. Accessed 24 Oct 2013
[22] Utting M, Legeard B (2007) Practical model-based testing—a tools approach. Morgan Kaufmann, San Francisco
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.