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

详细信息    查看全文

• 作者：Jianghua Lv ; Shilong Ma ; Xianjun Li ; Jiangong Song
• 关键词：safety critical systems (SCS) ; test ; automatic test ; equipment collaboration ; high order calculus ; LTS ; real time
• 刊名：Frontiers of Computer Science in China
• 出版年：2015
• 出版时间：August 2015
• 年：2015
• 卷：9
• 期：4
• 页码：495-510
• 全文大小：1,796 KB
• 参考文献：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鈥?51
  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鈥?657View Article
  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鈥?334View Article
  4.Bowen J, Stavridou V. Safety-critical systems, formal methods and standards. Software Engineering Journal, 1993, 8: 189鈥?09View Article
  5.Yoo J, Jee E, Cha S. Formal Modeling and Verification of Safety- Critical Software. 2009, 26(3): 42鈥?9
  6.Mitchell T R. A standard test language-GOAL (ground operations aerospace language). In: Proceedings of the 10th Design Automation Workshop. 1973: 87鈥?6
  7.Garner J T. Satellite Control: A Comprehensive Approach. JohnWiley, 1996
  8.Inc S. EPOCH T&C STOL Programmer鈥檚 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鈥?81
  11.TechSAT GmbH. ADS2 鈥?Avionics Development System 2nd Generation, 2014 http://鈥媤ww.鈥媡echsat.鈥媍om/鈥媐ileadmin/鈥媘edia/鈥媝df/鈥婣DS2_鈥?ProductOv-erview/TechSAT_PD_ADS2_CN_1000.pdf
  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鈥?79View Article
  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鈥?87View Article
  17.Maurer P M. The design and implementation of a grammar-based data generator. Software: Practice and Experience, 1992, 22: 223鈥?44
  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鈥?27View Article
  19.Tretmans J. Model based testing with labelled transition systems. Lecture Notes in Computer Science, 2008, 4949: 1鈥?8MathSciNet View Article
  20.Abdurazik A, Offutt J. Using UML collaboration diagrams for static checking and test generation. Lecture Notes in Computer Science, 2000: 383鈥?95
  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鈥?24View Article
  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鈥?99View Article
  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鈥?03MathSciNet View Article
  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鈥?76MathSciNet View Article
  26.Thomsen. A theory of higher order communicating systems. Information and Computation, 1995, 116: 38鈥?7MathSciNet View Article
  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鈥揂 concurrent calculus for higher-order communicating systems. Journal of Beijing University of Aeronautics and Astronautics, 1992, 1992: 12鈥?8
  29.Cardelli L, Gordon A D. Mobile ambients. Theoretical Computer Science, 2000, 240: 177鈥?13MathSciNet View Article
  30.Degano P, Loddo J V, Priami C. Mobile processes with local clocks. Analysis and Verification of Multiple-Agent Languages, 1997: 296鈥?19View Article
  31.Berger M. Basic Theory of reduction congruence for two timed asynchronous p-Calculi. Lecture Notes in Computer Science, 2004, 3170: 115鈥?30View Article
  32.Tao Y, Du C L, Wang X W, Zheng W. A new component-based realtime system based on timed high-order (THO) p calculus. Journal of Northwestern Polytechnic University, 2009, 27(6): 906鈥?11
  33.Milner R, Parrow J, Walker D. A calculus of mobile processes, (Parts I and II). Information and Computation, 1992, 100: 41鈥?7MathSciNet View Article
  34.Tretmans J. Conformance testing with labelled transition systems: implementation relations and test generation. Computer Networks and ISDN Systems, 1996, 29: 49鈥?9View Article
  35.Li W, Ma S. Limits of theory sequences over algebraically closed fields and applications. Discrete Applied Mathematics, 2004, 136: 23鈥?3MathSciNet View Article
  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鈥?3
  
• 作者单位：Jianghua Lv (1)
  Shilong Ma (1)
  Xianjun Li (1)
  Jiangong Song (1)
  
  1. State Key Lab of Software Development Environment, School of Computer Science, Beihang University, Beijing, 100191, China
  
• 刊物类别：Computer Science
• 刊物主题：Computer Science, general
  Chinese Library of Science
  
• 出版者：Higher Education Press, co-published with Springer-Verlag GmbH
• ISSN：1673-7466

文摘

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.