Formal verification of complex systems based on SysML functional requirements

As modern systems continue to increase in size and complexity, they pose increasingly significant safety and risk management challenges. A model-based safety approach is an efficient way of coping with the increasing system complexity. It helps better manage the complexity by utilizing reasoning tools that require abstract models to detect failures as early as possible during the design process. This paper develops a methodology for the verification of safety requirements for design of complex engineered systems. The proposed approach combines a SysML modeling approach to document and structure safety requirements, and an assume-guarantee technique for the formal verification purpose. The assume guarantee approach, which is based on a compositional and hierarchical reasoning combined with a learning algorithm, is able to simplify complex design verification problems. The objective of the proposed methodology is to integrate safety into early design stages and help the system designers to consider safety implications during conceptual design synthesis, reducing design iterations and cost. The proposed approach is validated on the quad-redundant Electro-Mechanical Actuator (EMA) of a Flight Control Surface (FCS) of an aircraft.