This paper presents a novel safety specification and verification approach based on the compositional reasoning and model checking algorithms. The behavioral specification of each component and subsystem is modeled to describe the overall structure of the design. Then, these specifications are analyzed to determine the least number of component redundancies that are required to tolerate and prevent catastrophic system failure. The framework utilizes Labelled Transition Systems (LTS) formalism to model the behavior of components and subsystems. Furthermore, compositional analysis is used to reason about the components’ constraints (or assumptions) on their environments and the properties (or guarantees) of their output. This identification of local safety properties of components and subsystems leads to satisfaction of the desired safety requirements for the global system. A model of quad-redundant Electro-Mechanical Actuator (EMA) is constructed and, in an iterative approach, its safety properties are analyzed. Experimental results confirm the feasibility of the proposed approach for verifying the safety issues associated with complex systems in the early stages of the design process.
Multi-parameterised compositional verification of safety properties