How the story of UniTESK technology applications mirrors development of model based testing
Abstract
UniTESK (UNIfied TEsting and Specification toolKit) is a testing technology based on formal models (or specifications) of requirements to behavior of software or hardware components. It was created with experience gained during development of the framework for automated testing of a real-time operating system kernel during 1994-2000. Software contracts were the main kind of models in the first version of the technology. Automata models were also implemented to support generation of complicated test sequences. UniTESK was first used in 2000 in the development of the test suite for IPv6 implementation. It was the first experience of using contract specifications in testing of implementations of telecommunication protocols. This project demonstrated that contract specifications in combination with the technique of testing software systems with asynchronous interface developed within UniTESK are very effective. Applications of UniTESK to testing software components in Java include the project on testing of implementation of standard library for Java runtime support and the project on testing of infrastructure of information system for one of large mobile operators in Russia. The most significant application of UniTESK happened in 2005-2007 in the Open Linux Verification project. Formal specifications and tests for interfaces of the Linux Standard Base were created during the project. These results then were used in development of the test suite for Russian avionics real-time operating system. Positive lessons learned during development and using UniTESK include effective application of model based testing methods in large industrial projects, high level of test coverage achieved by the generated tests, applicability of model based testing to critical systems and applications. Negative lessons include the lack of well-defined and detailed models and specifications, extra development expenses caused by creation of test specific models, problems with introduction of model based testing technologies using bilingual test generation systems and specific notations.
About the Authors
V. P. Ivannikov
ISP RAS, Moscow
Russian Federation
Russian Federation
A. K. Petrenko
ISP RAS, Moscow
Russian Federation
Russian Federation
V. V. Kuliamin
ISP RAS, Moscow
Russian Federation
Russian Federation
A. V. Maksimov
ISP RAS, Moscow
Russian Federation
Russian Federation
References
1. Bourdonov, I.B., Kossatchev, A.S., Kuliamin, V.V., Petrenko, A.K.: UniTesK Test Suite Architecture. In: FME 2002. LNCS, vol. 2391, pp. 77-88. Springer-Verlag (2002)
2. V. V. Kuliamin, A. K. Petrenko, A. S. Kossatchev, I. B. Burdonov: The UniTesK Approach to Designing Test Suites. Programming and Computer Software, 29(6), 310-322 (2003)
3. Bourdonov, I.B, Kossatchev, A.S., Petrenko, A.K., Galter. D.: KVEST: Automated Generation of Test Suites from Formal Specifications. In: Proceedings of Formal Method Congress, Toulouse, France, 1999. LNCS, vol. 1708, pp. 608-621 (1999)
4.
5. Peleska, J.: Industrial-Strength Model-Based Testing – State of the Art and Current Challenges. Invited Talk. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing (MBT 2013), Rome, Italy, 17th March 2013. Electronic Proceedings in Theoretical Computer Science, 111, pp. 3–28. DOI: 10.4204/EPTCS.111.1 (2013)
6. Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag (2003)
7. UniTESK technology, http://unitesk.ispras.ru
8. OLVER project, http://linuxtesting.org
9. Microsoft Interoperability Initiative, http://www.microsoft.com/openspecifications
10. N. V. Pakulin, A. V. Khoroshilov: Development of formal models and conformance testing for systems with asynchronous interfaces and telecommunications protocols. Programming and Computer Software, 33 (6), 316-335 (2007)
11. A. V. Khoroshilov: Specifikacija i testirovanie komponentov s asinhronnymi interfesami [Specification and testing of components with asynchronous interfaces]. Dissertacija na stepen' k.f.-m.n. [PhD Thesis], Moskva (2006)
12. Kuliamin, V.V., Petrenko, A.K., Pakulin, N.V.: Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. In: Proceedings of WMSCI'2005, Orlando, USA, July 10-13, 2005. Model Based Development and Testing, v. VII, pp. 65-70 (2005)
13. Bourdonov, I.B., Demakov A.V., Jarov, A.A., Kossatchev, A.S., Kuliamin, V.V., Petrenko, A.K., Zelenov, S.V.: Java Specification Extension for Automated Test Development. In: Proceedings of PSI'01. LNCS, vol. 2244, pp. 301-307. Springer-Verlag (2001)
14. The Linux Foundation consortium. LSB certification test suite, http://ispras.linuxbase.org/index.php/LSB_Certification_System
15. Maksimov, A.V.: Requirements-based conformance testing of ARINC 653 real-time operating systems. In: Proceedings of the Data Systems In Aerospace (DASIA 2010) conference, 2010. ESA SP-682, ISBN 978-92-9221-246-9 (2010)
16. V. P. Ivannikov, A. S. Kamkin, A. S. Kossatchev, V. V. Kuliamin, A. K. Petrenko: The use of contract specifications for representing requirements and for functional testing of hardware models. Programming and Computer Software, 33(5), 272-282 (2007).
17. Chupilko, M.M.: Developing Test Systems of Multi-Modules Hardware Designs. ISSN 0361-7688, Programming and Computer Software, 2012, Vol. 38, No. 1, pp. 34-42. Pleiades Publishing, Ltd. (2012)
18. Zelenov, S.V., Zelenova, S.A.: Model-Based Testing of Optimizing Compilers. In: Proc. of the 19th IFIP TC6/WG6.1 International Conference on Testing of Software and Communicating Systems – 7th International Workshop on Formal Approaches to Testing of Software (TestCom/FATES 2007). LNCS, vol. 4581, pp. 365-377. Springer-Verlag, Berlin (2007)
19. Zelenov, S.V., Silakov, D.V., Petrenko, A.K., Conrad, M., Fey I.: Automatic Test Generation for Model-Based code Generators. In: IEEE ISoLA 2006 Second Intern. Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Paphos, Cyprus, pp. 68-75 (2006)
20. A. S. Kamkin: Metod avtomatizacii imitacionnogo testirovanija mikroprocessorov konvejernoj arhitektury na osnove formal'nyh specifikacij [Method for automating simulation testing microprocessor pipeline architecture based on formal specifications]. Dissertacija na stepen' k.f.-m.n. [PhD Thesis], Moskva (2009)
21. E. V. Kornykhin: Metod avtomatizacii generacii testovyh programm dlja verifikacii MMU [Method for automating simulation testing method microprocessors automation test program generation for verification of MMU]. Dissertacija na stepen' k.f.-m.n. [PhD Thesis], Moskva (2010)
22. Kamkin, A.S., Tatarnikov, A.: MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. In: Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2012), May 30-31, 2012, Perm, Russia (2012)
23. MBT survey, http://www.robertvbinder.com/docs/arts/MBT-User-Survey.pdf
24. Grieskamp, W.: Microsoft’s Protocol Documentation Program: A Success Story for Model-Based Testing. In: Testing – Practice and Research Techniques. Lecture Notes in Computer Science, vol. 6303, p. 7 (2010)
25. Adams, C.: Safety-critical software for mission-critical applications to get boost with release of DO-178C. Military & Aerospace Electronics, 10 (2010)
26. Common Criteria, http://www.commoncriteriaportal.org
27. SpecExplorer, http://research.microsoft.com/en-us/projects/specexplorer
28. The Java Modelling Language (JML), http://www.eecs.ucf.edu/~leavens/JML/index.shtml
29. Pakulin, N.V.: Integrated Modular Avionics: New Challenges for MBT. In: ETSI TTCN-3 User Conference and Model Based Testing Workshop, Bangalore, India, 11-14 June 2012 (2012)
30. Code Contracts, http://research.microsoft.com/en-us/projects/contracts
31. C++TESK, http://forge.ispras.ru/projects/cpptesk-toolkit
32. V. V. Kuliamin: Component architecture of model-based testing environment. Programming and Computer Software, 36(5), 289-305 (2010)
33. Kuliamin, V.V.: Multi-paradigm Models as Source for Automated Test Construction. In: Proceedings of the 1-st Workshop on Model Based Testing (MBT'2004, in ETAPS'2004), Barcelona, Spain, March 27-38, 2004, Electronic Notes in Theoretical Computer Science, 111:137-160, Elseveir, (2005)
34. ReQuality tool, http://requality.org/en/doc.en.html
35. Khoroshilov, A.V., Albitskiy, D., Koverninskiy, I.V., Olshanskiy, M.Yu., Petrenko, A.K., Ugnenko, A.A.: AADL-Based Toolset for IMA System Design and Integration. SAE Int. J. Aerosp. 5(2), DOI:10.4271/2012-01-2146 (2012)
36. Systems Modeling Language (SysML), http://www.sysml.org
37. Petrenko, A.K., Kuliamin, V.V., Maksimov A.V.: UniTESK: Component Model Based Testing. Proceedings of ICTERI 2013.
Review
For citations:
Ivannikov V.P., Petrenko A.K., Kuliamin V.V., Maksimov A.V. How the story of UniTESK technology applications mirrors development of model based testing. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2013;24. (In Russ.)
Email this article 