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

doi:10.1007/s11704-015-2254-y

Front. Comput. Sci.

2015, Vol. 9

Issue (4) : 495-510 https://doi.org/10.1007/s11704-015-2254-y

RESEARCH ARTICLE

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

Jianghua LV(

), Shilong MA, Xianjun LI, Jiangong SONG

State Key Lab of Software Development Environment, School of Computer Science, Beihang University, Beijing 100191, China

Download: PDF(1553 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Jianghua LV

Just Accepted Date: 31 December 2014 Issue Date: 07 September 2015

Cite this article:

Jianghua LV,Shilong MA,Xianjun LI, et al. A high order collaboration and real time formal model for automatic testing of safety critical systems[J]. Front. Comput. Sci., 2015, 9(4): 495-510.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-2254-y
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I4/495

1	K Liu, Z G Shan, J Wang, J F He, Z T Zhang, Y W Qin. Overview on major research plan of trustworthy software. Bulletin of national natural science foundation of China, 2008, 22: 145−151
2	Z Zheng, S Ma, W Li, X Jiang, W Wei, L Ma, S Tang. Complexity of software trustworthiness and its dynamical statistical analysis methods. Science in China Series F: Information Sciences, 2009, 52: 1651−1657 https://doi.org/10.1007/s11432-009-0143-4
3	Z Zheng, S Ma, W Li, W Wei, X Jiang, Z Zhang, B Guo. Dynamical characteristics of software trustworthiness and their evolutionary complexity. Science in China Series F: Information Sciences, 2009, 52: 1328−1334 https://doi.org/10.1007/s11432-009-0137-2
4	J Bowen, V Stavridou. Safety-critical systems, formal methods and standards. Software Engineering Journal, 1993, 8: 189−209 https://doi.org/10.1049/sej.1993.0025
5	J Yoo, E Jee, S Cha. Formal Modeling and Verification of Safety-Critical Software. 2009, 26(3): 42−49
6	T R Mitchell. A standard test language-GOAL (ground operations aerospace language). In: Proceedings of the 10th Design Automation Workshop. 1973: 87−96
7	J T Garner. Satellite Control: A Comprehensive Approach. JohnWiley, 1996
8	S Inc. EPOCH T&C STOL Programmer’s Reference Manual. Integral Systems Inc, 1992
9	S C Committee. ATLAS 2000 Requirements Document, Revision 2.1. New York: IEEE, 1996
10	J Gil, B Holstein. 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	J Zhang. Study of automatic test language for spacecraft application system. Dissertation for Master Degree, Beijing: Graduate University of Chinese Academy of Sciences, 2005
13	Z Li. 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	G Yu, J Xue, Z Du. Research on scenario-event-driven simulation test script language for safety-critical software system. Journal of Computer Applications, 2010, 30: 374−379 https://doi.org/10.3724/SP.J.1087.2010.00374
15	D Yu, S Ma. Spacecraft Automatic Test Language and System. National Defense Industry Press, 2011
16	T S Chow. Testing software design modeled by finite-state machines. IEEE Transaction on Software Engineering 1978, 4: 178−187 https://doi.org/10.1109/TSE.1978.231496
17	P M Maurer. The design and implementation of a grammar-based data generator. Software: Practice and Experience, 1992, 22: 223−244 https://doi.org/10.1002/spe.4380220303
18	H Hong, Y Kim, S Cha. A test sequence selection method for state charts. The Journal of Software Testing, Verification & Reliability, 2000, 10: 203−227 https://doi.org/10.1002/1099-1689(200012)10:4<203::AID-STVR212>3.0.CO;2-2
19	J Tretmans. Model based testing with labelled transition systems. Lecture Notes in Computer Science, 2008, 4949: 1−38 https://doi.org/10.1007/978-3-540-78917-8_1
20	A Abdurazik, J Offutt. Using UML collaboration diagrams for static checking and test generation. Lecture Notes in Computer Science, 2000: 383−395 https://doi.org/10.1007/3-540-40011-7_28
21	J A Whittaker, M Thomason. A Markov chain model for statistical software testing. In: Proceedings of IEEE Transactions on Software Engineering, 1994, 20(10): 812−824 https://doi.org/10.1109/32.328991
22	J H Poore. Introduction to the special issue on: model-based statistical testing of software intensive systems. Information and Software Technology, 2000, 42(12): 797−799 https://doi.org/10.1016/S0950-5849(00)00138-5
23	M Memon. A comprehensive framework for testing graphical user interfaces. Dissertation for PhD Degree, University of Pittsburgh, 2001
24	S Konur. A survey on temporal logics for specifying and verifying realtime systems. Frontiers of Computer Science, 2013, 7(3): 370−403 https://doi.org/10.1007/s11704-013-2195-2
25	X X Yang, Y Zhang, M Fu, X Y Feng. A temporal programming model with atomic blocks based on projection temporal logic. Frontiers of Computer Science, 2014, 8(6): 958−976 https://doi.org/10.1007/s11704-014-3342-0
26	Thomsen. A theory of higher order communicating systems. Information and Computation, 1995, 116: 38−57 https://doi.org/10.1006/inco.1995.1004
27	D Sangiorgi. Expressing mobility in process algebras: first-order and higher-order paradigms. Dissertation for PhD Degree, Edinburgh: University of Edinburgh, 1992
28	J Wang, W Li. CC−A concurrent calculus for higher-order communicating systems. Journal of Beijing University of Aeronautics and Astronautics, 1992, 1992: 12−18
29	L Cardelli, A D Gordon. Mobile ambients. Theoretical Computer Science, 2000, 240: 177−213 https://doi.org/10.1016/S0304-3975(99)00231-5
30	P Degano, J V Loddo, C Priami. Mobile processes with local clocks. Analysis and Verification of Multiple-Agent Languages, 1997: 296−319 https://doi.org/10.1007/3-540-62503-8_14
31	M Berger. Basic Theory of reduction congruence for two timed asynchronous π-Calculi. Lecture Notes in Computer Science, 2004, 3170: 115−130 https://doi.org/10.1007/978-3-540-28644-8_8
32	Y Tao, C L Du, X W Wang, W Zheng. A new component-based realtime system based on timed high-order (THO) π calculus. Journal of Northwestern Polytechnic University, 2009, 27(6): 906−911
33	R Milner, J Parrow, D Walker. A calculus of mobile processes, (Parts I and II). Information and Computation, 1992, 100: 41−77 https://doi.org/10.1016/0890-5401(92)90009-5
34	J Tretmans. Conformance testing with labelled transition systems: implementation relations and test generation. Computer Networks and ISDN Systems, 1996, 29: 49−79 https://doi.org/10.1016/S0169-7552(96)00017-7
35	W Li, S Ma. Limits of theory sequences over algebraically closed fields and applications. Discrete Applied Mathematics, 2004, 136: 23−43 https://doi.org/10.1016/S0166-218X(03)00196-3
36	S Ma, X Li, B Sun, G Ye, Z Li, J Lv. 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

[1]

Supplementary Material-Highlights in 3-page ppt

Download

[1]	Ismael RODRÍGUEZ, David RUBIO, Fernando RUBIO. Complexity of adaptive testing in scenarios defined extensionally[J]. Front. Comput. Sci., 2023, 17(3): 173206-.
[2]	Bin ZHANG, Jiaxi YE, Ruilin LI, Chao FENG, Yunfei SU, Chaojing TANG. Pusher: an augmented fuzzer based on the connection between input and comparison operand[J]. Front. Comput. Sci., 2022, 16(4): 164206-.
[3]	Pengfei GAO, Yongjie XU, Fu SONG, Taolue CHEN. Model-based automated testing of JavaScript Web applications via longer test sequences[J]. Front. Comput. Sci., 2022, 16(3): 163204-.
[4]	Shahbaz ALI, Hailong SUN, Yongwang ZHAO. Model learning: a survey of foundations, tools and applications[J]. Front. Comput. Sci., 2021, 15(5): 155210-.
[5]	Dongjie CHEN, Yanyan JIANG, Chang XU, Xiaoxing MA. On interleaving space exploration of multi-threaded programs[J]. Front. Comput. Sci., 2021, 15(4): 154206-.
[6]	Shahid AKBAR, Maqsood HAYAT, Muhammad IQBAL, Muhammad TAHIR. iRNA-PseTNC: identification of RNA 5-methylcytosine sites using hybrid vector space of pseudo nucleotide composition[J]. Front. Comput. Sci., 2020, 14(2): 451-460.
[7]	Xin CHEN, He JIANG, Zhenyu CHEN, Tieke HE, Liming NIE. Automatic test report augmentation to assist crowdsourced testing[J]. Front. Comput. Sci., 2019, 13(5): 943-959.
[8]	Thierry GAUTIER, Clément GUY, Alexandre HONORAT, Paul LE GUERNIC, Jean-Pierre TALPIN, Loïc BESNARD. Polychronous automata and their use for formal validation of AADL models[J]. Front. Comput. Sci., 2019, 13(4): 677-697.
[9]	Xiaobing SUN,Xin PENG,Bin LI,Bixin LI,Wanzhi WEN. IPSETFUL: an iterative process of selecting test cases for effective fault localization by exploring concept lattice of program spectra[J]. Front. Comput. Sci., 2016, 10(5): 812-831.
[10]	Dan HAO,Lu ZHANG,Hong MEI. Test-case prioritization: achievements and challenges[J]. Front. Comput. Sci., 2016, 10(5): 769-777.
[11]	Xiaofang QI,Jun HE,Peng WANG,Huayang ZHOU. Variable strength combinatorial testing of concurrent programs[J]. Front. Comput. Sci., 2016, 10(4): 631-643.
[12]	Priyanka CHAWLA,Inderveer CHANA,Ajay RANA. A novel strategy for automatic test data generation using soft computing technique[J]. Front. Comput. Sci., 2015, 9(3): 346-363.
[13]	Yan ZHANG,Dunwei GONG. Generating test data for both paths coverage and faults detection using genetic algorithms: multi-path case[J]. Front. Comput. Sci., 2014, 8(5): 726-740.
[14]	Chang-ai SUN,Zuoyi WANG,Guan WANG. A property-based testing framework for encryption programs[J]. Front. Comput. Sci., 2014, 8(3): 478-489.
[15]	Dunwei GONG, Yan ZHANG. Generating test data for both path coverage and fault detection using genetic algorithms[J]. Front Comput Sci, 2013, 7(6): 822-837.

Viewed

Full text

Abstract

Cited

Shared

Discussed