MC/DC Test Case Generation Method Based On Safety＿SysML Safety State Machine

Ensuring safety and reliability is a key objective in the design of safety-critical systems.Due to their complex structure,high degree of concurrency,and the pres-ence of uncertain stochastic behaviors,efficient testing of such systems has become a challenge.Model-based testing,which generates test cases automatically from the sys-tem requirements model,is one of the feasible approaches to address this challenge.In model-based test case generation techniques,the selection of models needs to be de-termined based on the system requirements.Among the existing modeling languages,Systems Modeling Language(Sys ML)is a generic graphical modeling language that can be used to design and validate complex systems.Although Sys ML has well-defined syntactic rules,it lacks precise semantic de-scriptions,making its semantics still informal.Therefore,the state machine diagrams defined by Sys ML cannot be directly applied to formal analysis,and the safety of the state machine model itself cannot be guaranteed.Additionally,most model-based test-ing generation techniques often focus on the model itself,ignoring the real-time envi-ronment in which the system model operates.Furthermore,as the complexity of the system model increases,the number of generated test case sets can be very large,and it may not be possible to effectively detect defects in the system model using the test case sets.To address these issues,we selected a formal modeling language,Safety＿Sys ML Safety State Machine(S~2M SM),as the research object to study the method of gener-ating test cases based on this model.The main research work and contributions of this thesis are as follows:(1)Based on the syntax and semantics of the S~2M SM modeling language,we constrained certain modeling elements and established an S~2M SM model according to system requirements.We then conducted formal verification of the model,resulting in a reliable model;(2)The structure of the S~2M SM model is complex,and existing test case genera-tion techniques cannot be directly applied to models with complex structures.Therefore,we proposed a model transformation algorithm that focuses on the composite states and loops in the S~2M SM model.This algorithm generates an intermediate model that is suitable for testing;(3)We designed a time sequence operation module based on the definition of S~2M SM,which simulates the real-time external environment.The time sequence op-eration module and the model are continuously synchronized during the test case gen-eration process.Therefore,we proposed a novel test case generation method that uses the time sequence operation module and the intermediate model as input parameters.Guided by the time sequence operation module,the S~2M SM model communicates synchronously and generates corresponding test cases;(4)In the process of test case generation,we chose the Modified Condition/De-cision Coverage Criterion(MC/DC)as the test coverage strategy,which is currently less researched.It greatly reduces the number of generated test cases while meeting the testing requirements of safety-critical systems.To demonstrate the feasibility and effectiveness of the proposed method,this paper describes the application of the test case generation technique based on the S~2M SM model in the rocket launch abort system as an example in the aerospace system.