Formal Verification of Complex Systems based on SysML Functional Requirements

As modern systems continue to increase in size and complex-ity, they pose increasingly significant safety and risk manage-ment challenges. A model-based safety approach is an effi-cient 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 ap-proach 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 con-sider safety implications during conceptual design synthesis, reducing design iterations and cost. The proposed approach is validated on the quad-redundant Electro-Mechanical Actu-ator (EMA) of a Flight Control Surface (FCS) of an aircraft. 1