Research On Component-based Embedded Software Safety Analysis Methods

As embedded software systems are ubiquitous in our daily lives, such as automotive, energy industries and aerospace. Failures of these systems will cause pollution of environment, property losses and even casualties. As a result, safety analyses have been critical for developing these systems.For the size and complexity of these systems have been increasing rapidly, software architectures of them are distributed and component-based. Consequently, safety analyses for component-based embedded software systems are important methods and hot research issues in embedded software development. Although most of traditional safety analysis methods can be applied in requirement analysis phrase, there are still no suitable safety analysis methods and tools that can be used in software design phrase.Formal methods are mathematically-based approaches to the specification, analysis and verification of system behavior, both software and hardware. As a result of high safety demand of embedded software systems, it is effective to increase the software safety by using formal analysis technology. Consequently, introducing formal methods in analyzing embedded software safety in design phrase can increase the safety of embedded software effectively.In this thesis, we focus on the problem of safety modeling and analysis for component-based embedded software system design. We first use Sys ML and state/event fault tree to model safety design models of embedded software systems. Then based on these safety design models, we perform safety analysis for both software static structure and dynamic failure behavior respectively. The main contributions of this thesis are as follows:(1) In order to analyze the consistency of static structure safety level dependence and safety certification standard requirements, we first capture the objectives of safety level dependence requirements from DO-178 B, and then construct the safety design model of system static structure based on Sys ML block definition diagram. As Sym ML block definition diagram is semi-formal, we propose block dependency diagram to formally describe precise semantics of it. After that, we present a consistency algorithm to analyze the conformance of system static structure’s safety level dependence and certification objectives. The integrated safety level of systems can be promoted by applying this method, and the process and result of this method can be used as safety certitification evidence.(2) In order to analyze minimal cut sequences of cause-effect chains for component-basedembedded software system’ dynamic failure behaviors, we first use state/event fault tree to model cause-effect chains of systems’ failure behaviors. As state/event fault tree lack of precise semantics,we then propose guarded interface automata to describe formal semantics of state/event fault tree’s behaviors. Furthermore, we give a parallel composition and aggregation framework to generate formal semantics for state/event fault tree. During this composition process, we define weak bisimulation operation to reduce state space. After that, minimal cut sequences generation method of state/event fault tree is presented. The analysis result of this appraoch can provide support for software test case generation and model checking.(3) In order to analyze safety parameters of dynamic failure behaviors, such as probabilistic and time parameters, we use state/event fault tree to model cause-effect chains of systems’ failure behaviors. As state/event fault tree can both model dynamic failure behavior and probability information of systems, we can further analyze probabilistic and time parameters based on minimal cut sequences. For state/event fault tree lack of precise semantics, we first propose interface interactive markov chain to both describe behavior and probabilistic information of state/event fault tree. Then we propose a parallel composition and aggregation framework to obtain formal semantics of state/event fault tree. During this composition process, we define weak bisimulation operation for interface interactive markov chain to reduce state space. After that we use existing probabilistic analysis tool MRMC and IMCA to analyze probabilistic and time properties of state/event fault tree respectively, and these analysis results can be used in software safety evaluation.(4) And a tool, named T-CESSA(Tool for component-based embedded software safety analysis)is designed based on the above proposed approaches to support analyzing safety level dependence of software static structure, analyzing minimal cut sequences for dynamic failure behaviors, and quantitatively analyzing probabilistic and time properties of dynamic failure behaviors. After that,three typical embedded software system case studies are presented to illustrate the effectiveness of the methods proposed above.