The final models of specification

The paper describes the research in formal methods of conformance testing of the target system against requirements given in specifications. Such testing is based on interaction semantics defining test stimuli and observations of actions and refusals (absence of actions). Unobservable actions and refusals are also possible. Destruction is introduced as a forbidden action that should be avoided during interaction. A notion of safe testing is also introduced, when no unobservable refusals and destruction occur and no test stimuli applied in divergence. On this basis, the implementation hypothesis of safety and safe conformance are defined, as well as the generation of complete test suite from specification.

The most common model of specification is LTS (Labelled Transition System). However, for the described interaction semantics, only traces (sequences of observations) are important, not the LTS states. Therefore, the most natural is the trace model defined as a set of LTS traces.

The goal of this paper is to define the subset of specification traces sufficient for generation of the complete test suite. We called such subset the final trace model of specification. On the other hand, LTS model is convenient as a way of finite representation of regular trace sets. To represent the final trace model, the paper proposes a variation of LTS called final RTS (Refusal Transition System). The transitions on observable refusals are defined explicitly. Such model is very convenient for test generation: 1) it is deterministic, 2) trace of observations is safe iff it ends in non-terminal state with no destruction, 3) test stimulus is safe after the trace iff it is safe in the final state of the trace.

The paper proposes algorithms for transformation of LTS model into final RTS model. Sufficient conditions for creation of the final RTS in finite time are also defined.

interaction semantics, refusals, destruction, divergence, conformance, safe testing, traces, LTS, test generation

1. Bourdonov I., Kossatchev A., Kuliamin V. Formal Conformance Testing of Systems with Refused Inputs and Forbidden Actions. Proc. of MBT 2006, Vienna, Austria, March 2006.

2. Bourdonov I., Kossatchev A., Kuliamin V. Formalization of Test Experiments. Programming and Computer Software, Vol. 33, No. 5, 2007, pp. 239-260

3. Bourdonov I., Kossatchev A., Kuliamin V. Bezopasnost', verifikatsiya i teoriya konformnosti [Safety, Verification and Conformance Theory]. Materialy Vtoroj mezhdunarodnoj nauchnoj konferentsii po problemam bezopasnosti i protivodejstviya terrorizmu [The proceeding of the Second international conference on the problems of safety and counteraction against terrorizm], Moscow, MNCMO, 2007. pp. 135-158. (in Russian).

4. Bourdonov I., Kossatchev A., Kuliamin V. Teoriya sootvetstviya dlya system s blokirovkami I razrusheniem [Conformance theory of the systems with Refused Inputs and Forbidden Actions]. Moscow, «Nauka», 2008, 412 p. (in Russian)

5. Bourdonov I. Teoriya konformnosti (funkcional'noe testirovanie prorammny'kh system na osnove formal'ny'kh modelej [Conformance theory (functional testing on formal model base)]. LAP LAMBERT Academic Publishing, Saarbrucken, Germany, 2011, ISBN 978-3-8454-1747-9, 428 pp. http://www.ispras.ru/~RedVerst/RedVerst/Publications/TR-01-2007.pdf) (in Russian)

6. Bourdonov I., Kossatchev A. Sistemy s prioritetami: konformnost', testirovanie, kompozitsiya [Systems with priority: conformance, testing, composition]. Trudy ISP RAN [The proceeding of ISP RAS], Vol. 14.1, 2008, pp.23-54. (in Russian)

7. Bourdonov I., Kossatchev A. Ehkvivalentnye semantiki vzaimodejstviya [Equivalent interaction semantics]. Trudy ISP RAN [The proceeding of ISP RAS], v. 14.1, 2008, pp.55-72. (in Russian)

8. Bourdonov I., Kossatchev A. Systems with Priorities: Conformance, Testing, and Composition. Programming and Computer Software, Vol. 35, No. 4, 2009, pp.198-211.

9. Bourdonov I., Kossatchev A. Аnaliticheskaya verifikatsiya konformnosti [Analitical conformance verification]. Nauchnyj servis v seti Internet: masshtabiruemost', parallel'nost', ehffektivnost': Trudy Vserossijskoj superkomp'yuternoj konferentsii (21-26 sentyabrya 2009 g., g. Novorossijsk) [Scientific service of Internet: The proceeding of Russian Supercomputer conference (21-26 sept. 2009, Novorossijsk)] – Moscow, MSU publ., 2009. (in Russian)

10. Bourdonov I., Kossatchev A. Testirovanie konformnosti na osnove sootvetstviya sostoyanij [Conformance testing based on a state relation]. Trudy ISP RAN [The proceeding of ISP RAS, Vol. 18, 2010, pp. 183-320. (in Russian)

11. Bourdonov I., Kossatchev A. Simulyatsiya sistem s otkazami i razrusheniem [Simulation of the systems with Refused Inputs and Forbidden Actions]. 5-yj Mezhdunarodnyj simpozium po komp'yuternym naukam v Rossii. Seminar «Semantika, spetsifikatsiya i verifikatsiya programm: teoriya i prilozheniya» [5-th International symposium on computer science in Russia. Workshop “Semanticsand program specification and verification: Theory and applications”]. Kazan' 2010. (in Russian)

12. Bourdonov I., Kossatchev A. Testirovanie bezopasnoj simulyatsii [Safe simulation testing]. 5-yj Mezhdunarodnyj simpozium po komp'yuternym naukam v Rossii. Seminar «Semantika, spetsifikatsiya i verifikatsiya programm: teoriya i prilozheniya» [5-th International symposium on computer science in Russia. Workshop “Semanticsand program specification and verification: Theory and applications”]. Kazan' 2010. (in Russian)

13. Bourdonov I., Kossatchev A. Semantiki vzaimodejstviya s otkazami, divergentsiej i razrusheniem. CHast' 1. Gipoteza o bezopasnosti i bezopasnaya konformnost'. [Semantics of Interaction with Refused Inputs, Divergence and Forbidden Actions. Part 1. Hypothesis of safety and safe conformance]. «Vestnik Tomskogo gosudarstvennogo universiteta. Upravlenie, vychislitel'naya tekhnika i informatika» [Tomsk State University. Journal of Control and Computer Science]., №4, 2010. (in Russian)

14. I.Burdonov, A.Kosachev. Formal conformance verification. Short Papers of the 22nd IFIP ICTSS, Alexandre Petrenko, Adenilso Simao, Jose Carlos Maldonado (eds.), Nov. 08-10, 2010, Natal, Brazil.

15. Bourdonov I., Kossatchev A. Interaction Semantics with Refusals, Divergence, and Destruction. Programming and Computer Software, Vol. 36, No. 5, 2010, pp. 247-263.

16. Bourdonov I., Kossatchev A. Specification Completion for IOCO. Programming and Computer Software, Vol. 37, No. 1, 2011, pp. 1-14.

17. Bourdonov I., Kossatchev A. Udalenie iz spetsifikatsii nekonformnykh trass [Nonconforming traces elimination from specification]. Preprint № 23, ISP RАN [Preprints of the Institute for System Programming of RAS, Preprint 23], 2011. (in Russian)

18. Bernot G. Testing against formal specifications: A theoretical view. In S. Abramsky and T.S.E. Maibaum, editors, TAPSOFT’91, Volume 2, pp. 99-119. Lecture Notes in Computer Science 494, Springer-Verlag, 1991.

19. Edmonds J. Johnson E.L. Matching. Euler Tours, and the Chinese Postman. Math. Programming 5, 88-124 (1973).

20. van Glabbeek R.J. The linear time – branching time spectrum. In J.C.M. Baeten and J.W. Klop, editors, CONCUR’90, Lecture Notes in Computer Science 458, Springer-Verlag, 1990, pp 278–297.

21. van Glabbeek R.J. The linear time - branching time spectrum II; the semantics of sequential processes with silent moves. Proceedings CONCUR ’93, Hildesheim, Germany, August 1993 (E. Best, ed.), LNCS 715, Springer-Verlag, 1993, pp. 66-81.

22. Lee D., Yannakakis M. Principles and Methods of Testing Finite State Machines – A Survey. Proceedings of the IEEE 84, No. 8, 1090–1123, 1996.

23. Milner R. Modal characterization of observable machine behaviour. In G. Astesiano & C. Bohm, editors: Proceedings CAAP 81, LNCS 112, Springer, pp. 25-34.

24. Tretmans J. Conformance testing with labelled transition systems: implementation relations and test generation. Computer Networks and ISDN Systems, v.29 n.1, p.49-79, Dec. 1996.

25. Tretmans J. Test Generation with Inputs, Outputs and Repetitive Quiescence. In: Software-Concepts and Tools, Vol. 17, Issue 3, 1996.