A high order collaboration and real time formal model for automatic testing of safety critical systems

Abstract

The need for safety critical systems (SCS) is both important and urgent, and their evaluation and verification are test-dependent. SCS are usually complex and very large, so manual testing of SCS are infeasible in practice, and developing automatic test approaches for SCS has become an important trend. This paper defines a formal semantics model for automatic test of SCS, called AutTMSCS, which describes behaviors in SCS testing. The model accommodates the high order collaboration in real time and temporariness of SCS testing. Testing tasks, test equipment and products under test are abstracted and architected in three layers, and a method for automatic testing is given. Based on extended label transition system (LTS), the convergency and correctness of the model are proved to demonstrate the computability of the model, indicating that the testing process of SCS can be automatic.

Keywords

safety critical systems (SCS) / test / automatic test / equipment collaboration / high order calculus / LTS / real time

References

[1] Liu K, Shan Z G, Wang J, He J F, Zhang Z T, Qin Y W. Overview on major research plan of trustworthy software. Bulletin of national natural science foundation of China, 2008, 22: 145−151

[2] Zheng Z, Ma S, Li W, Jiang X, Wei W, Ma L, Tang S. Complexity of software trustworthiness and its dynamical statistical analysis methods. Science in China Series F: Information Sciences, 2009, 52: 1651−1657

[3] Zheng Z, Ma S, Li W, Wei W, Jiang X, Zhang Z, Guo B. Dynamical characteristics of software trustworthiness and their evolutionary complexity. Science in China Series F: Information Sciences, 2009, 52: 1328−1334

[4] Bowen J, Stavridou V. Safety-critical systems, formal methods and standards. Software Engineering Journal, 1993, 8: 189−209

[5] Yoo J, Jee E, Cha S. Formal Modeling and Verification of Safety-Critical Software. 2009, 26(3): 42−49

[6] Mitchell T R. A standard test language-GOAL (ground operations aerospace language). In: Proceedings of the 10th Design Automation Workshop. 1973: 87−96

[7] Garner J T. Satellite Control: A Comprehensive Approach. JohnWiley, 1996

[8] Inc S. EPOCH T&C STOL Programmer’s Reference Manual. Integral Systems Inc, 1992

[9] Committee S C. ATLAS 2000 Requirements Document, Revision 2.1. New York: IEEE, 1996

[10] Gil J, Holstein B. T++: a test case generator using a debugging information based technique for source code manipulation. In: Proceedings of Technology of Object-Oriented Languages and Systems. 1997: 272−281

[11] TechSAT GmbH. ADS2 — Avionics Development System 2nd Generation, 2014

[12] Zhang J. Study of automatic test language for spacecraft application system. Dissertation for Master Degree, Beijing: Graduate University of Chinese Academy of Sciences, 2005

[13] Li Z. Study of language for satellite testing and operation and its integrated support environment. Dissertation for Master Degree, Beijing: Graduate University of Chinese Academy of Sciences, 2004

[14] Yu G, Xue J, Du Z. Research on scenario-event-driven simulation test script language for safety-critical software system. Journal of Computer Applications, 2010, 30: 374−379

[15] Yu D, Ma S. Spacecraft Automatic Test Language and System. National Defense Industry Press, 2011

[16] Chow T S. Testing software design modeled by finite-state machines. IEEE Transaction on Software Engineering 1978, 4: 178−187

[17] Maurer P M. The design and implementation of a grammar-based data generator. Software: Practice and Experience, 1992, 22: 223−244

[18] Hong H, Kim Y, Cha S. A test sequence selection method for state charts. The Journal of Software Testing, Verification & Reliability, 2000, 10: 203−227

[19] Tretmans J. Model based testing with labelled transition systems. Lecture Notes in Computer Science, 2008, 4949: 1−38

[20] Abdurazik A, Offutt J. Using UML collaboration diagrams for static checking and test generation. Lecture Notes in Computer Science, 2000: 383−395

[21] Whittaker J A, Thomason M. A Markov chain model for statistical software testing. In: Proceedings of IEEE Transactions on Software Engineering, 1994, 20(10): 812−824

[22] Poore J H. Introduction to the special issue on: model-based statistical testing of software intensive systems. Information and Software Technology, 2000, 42(12): 797−799

[23] Memon M. A comprehensive framework for testing graphical user interfaces. Dissertation for PhD Degree, University of Pittsburgh, 2001

[24] Konur S. A survey on temporal logics for specifying and verifying realtime systems. Frontiers of Computer Science, 2013, 7(3): 370−403

[25] Yang X X, Zhang Y, Fu M, Feng X Y. A temporal programming model with atomic blocks based on projection temporal logic. Frontiers of Computer Science, 2014, 8(6): 958−976

[26] Thomsen. A theory of higher order communicating systems. Information and Computation, 1995, 116: 38−57

[27] Sangiorgi D. Expressing mobility in process algebras: first-order and higher-order paradigms. Dissertation for PhD Degree, Edinburgh: University of Edinburgh, 1992

[28] Wang J, Li W. CC−A concurrent calculus for higher-order communicating systems. Journal of Beijing University of Aeronautics and Astronautics, 1992, 1992: 12−18

[29] Cardelli L, Gordon A D. Mobile ambients. Theoretical Computer Science, 2000, 240: 177−213

[30] Degano P, Loddo J V, Priami C. Mobile processes with local clocks. Analysis and Verification of Multiple-Agent Languages, 1997: 296−319

[31] Berger M. Basic Theory of reduction congruence for two timed asynchronous π-Calculi. Lecture Notes in Computer Science, 2004, 3170: 115−130

[32] Tao Y, Du C L, Wang X W, Zheng W. A new component-based realtime system based on timed high-order (THO) π calculus. Journal of Northwestern Polytechnic University, 2009, 27(6): 906−911

[33] Milner R, Parrow J, Walker D. A calculus of mobile processes, (Parts I and II). Information and Computation, 1992, 100: 41−77

[34] Tretmans J. Conformance testing with labelled transition systems: implementation relations and test generation. Computer Networks and ISDN Systems, 1996, 29: 49−79

[35] Li W, Ma S. Limits of theory sequences over algebraically closed fields and applications. Discrete Applied Mathematics, 2004, 136: 23−43

[36] Ma S, Li X, Sun B, Ye G, Li Z, Lv J. Research and application of key technologies of general test language and system in automatic test of spacecraft. China Science and Technology Achievements, 2012, 13: 62−63

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg