Automatic Formal Verification of SysML State Machine Diagrams for Vehicular Control Systems

Vehicular control systems are characterized with numerous complex interactions with a steady rise of autonomous functions, which makes it more challenging for designers and safety engineers to identify unexpected failures. These systems tend to be highly integrated and exhibit features like concurrency for which traditional verification and validation techniques (i.e. testing and simulation) are insufficient to provide rigorous and complete assessment. Model Checking, a well-known formal verification technique, can be used to rigorously prove the correctness of such systems according to design Requirements. In particular, Model Checking is a method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Systems Modeling Language (SysML) has been widely used in architectural and functional modeling in automotive industries. However, it cannot directly be verified against safety requirements. In this work, SysML is used to establish a unified system model that can present an integrated autonomy software and hardware system of a vehicular control system. A generic model transformation strategy is developed to integrate SysML with one of the state-of-the-art Model Checking tools, NuSMV. Cameo Systems Modeler is an industry leading cross-platform collaborative Model-Based Systems Engineering environment for designing standard-compliant SysML models and diagrams. A native Cameo's plugin is constructed to transform SysML state machines to the input language of NuSMV model checker and also to replay the verification results back into the Cameo's environment. A case study of an executable state machine for a high-level autonomous driving system is built. The NuSMV model checker is used to model check the state machine of the autonomous driving system against design requirements expressed as temporal logic formulas. Upon violation of design requirements, our SysML-NuSMV integration allows to replay counterexamples in the Cameo modeling environment. Thus a bi-directional integration of system modeling language with the model checker is developed and the transformation rules are defined. The case study result shows how this method can help designers and safety engineers to automatically identify hidden design errors in a variety of possible design models.