Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas

Model Based Systems Engineering (MBSE) provides a single platform capable of defining complex, multidisciplinary systems, but commonly-used tools such as Systems Modeling Language (SysML) lack the ability to formally validate and verify these systems. Symbolic model checking operates on system models of similar levels of abstraction to SysML, providing a push-button technique for ensuring the possible behavior set always obeys temporal requirements, e.g., for safe operation. We propose a translation method from SysML activity diagrams to the popular symbolic model checker nuXmv to enable their formal verification in four main steps: main module definition, submodule definition, activity diagram organization, and activity diagram translation. We apply this process to the Autonomous Artificial Pancreas System (AAPS) as a trade study. We then verify and validate the AAPS nuXmv model against a set of specifications derived from the AAPS safety requirements.