Abstract
In this paper a virtual test method, which is a fusion approach on the combination of automata-based model checking theory and systems engineering theory, is proposed. An automaton of Window Tree Model (WTM) based on multi-tree to describe the system behavior as a system model is used on one hand, and a State Transition Graph (STG) based on Büchi automaton to describe design correctness as a specification is used on the other hand. An automaton-based model checking mechanism is designed to build the foundation of the virtual test method. Moreover, the two main aspects of the method, which are the design correctness verification and the interface test, are defined. A case study is followed to illustrate the modeling and verification process. Finally, a Virtual Test Platform (VTP), which implements the method, is introduced to unfold the virtual test configuration, virtual test execution as well as the virtual test evaluation features.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Chen M et al (2012) System-level validation: high-level modeling and directed test generation techniques
Garzon MH, Blain DR, Neel AJ (2004) Virtual test tubes. Nat Comput 3(4):461–477
Magnusson PS (2005) The Virtual Test Lab. Computer 38(5):95–97
Wang GG (2002) Definition and review of virtual prototyping. J Comput Inf Sci Eng 2(3):232–236
Baier C, Katoen JP (2008) Principles of model checking. Mit Press
Rowson JA (1997) Virtual prototyping. In: Proceedings of the IEEE 1997 Custom Integrated Circuits Conference
Huang T et al (2007) A virtual prototyping system for simulating construction processes. Automation in construction 16(5):576–585
Van der Auweraer H et al (2008) Breakthrough technologies for virtual prototyping of automotive and aerospace structures, pp 397–419
Wang Y, Wang L, Zheng Z (2012) Application of virtual prototype technology to simulation test for airborne software system. Springer, Berlin, pp 653–658
Gokdere LU et al (2002) A virtual prototype for a hybrid electric vehicle. Mechatronics 12(4):575–593(19)
Bezin Y et al (2015) Virtual testing environment tools for railway vehicle certification. Proc Inst Mech Eng Part F J Rail Rapid Transit 22(4):221–249
Heitmeyer C et al (2007) Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1):82–98
Clarke EM, Wing JM (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28(4):626–643
Carcenac F, Boniol F (2004) Verification of an avionic system using timed model checking. In: International symposium on leveraging applications of formal methods, ISoLA 2004, October 30–November 2, 2004, Paphos, Cyprus. Preliminary proceedings
Mota A, Sampaio A (2001) Model-checking CSP-Z: strategy, tool support and industrial application. Sci Comput Program 40(1):59–96
Bjørner N et al (1996) STeP: deductive-algorithmic verification of reactive and real-time systems. Springer, Berlin, pp 415–418
Li R et al (2015) Avionics system testing based on formal methods. J Softw 2:181–201
Lian H (2013) Research on key technology of test method for credibility validation of safety-critical system. In: Computer science. Beihang University, p 107
Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: Symposium on logic in computer science, 16–18 June 1986, Cambridge, Massachusetts, USA
Duarte EP, Ziwich RP, Albini LCP (2011) A survey of comparison-based system-level diagnosis. ACM Comput Surv 43(3):194–218
Vladimirova T, Sweeting M (2004) System-on-a-chip development for small satellite onboard data handling. J Aerosp Comput Inf Commun 1(1):36–43
Gross J (2009) An executable unified product model based on UML to support satellite design. AIAA J
Biafore B (2007) Visio 2007 Bible. Wiley
Acknowledgments
This work was supported by the National Natural Science Foundation of China under Grant Nos. 61300007 and 61305054, the Fundamental Research Funds for the Central Universities of China under Grant Nos. YWF-15-GJSYS-106 and YWF-14-JSJXY-007, and the Project of the State Key Laboratory of Software Development Environment of China under Grant Nos. SKLSDE-2015ZX-09 and SKLSDE-2014ZX-06.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer Science+Business Media Singapore
About this paper
Cite this paper
Wuniri, Q., Li, X., Yang, F., Ma, S., Liu, Y., Li, N. (2016). A Method of Virtual Test Based on Model Checking and a Case Study. In: Jia, Y., Du, J., Zhang, W., Li, H. (eds) Proceedings of 2016 Chinese Intelligent Systems Conference. CISC 2016. Lecture Notes in Electrical Engineering, vol 404. Springer, Singapore. https://doi.org/10.1007/978-981-10-2338-5_42
Download citation
DOI: https://doi.org/10.1007/978-981-10-2338-5_42
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-2337-8
Online ISBN: 978-981-10-2338-5
eBook Packages: Computer ScienceComputer Science (R0)