Automated SysML v2 System Model to Memory-Safe Language Code Generation for Avionics Applications

One of the greatest challenges of Model-Based Systems Engineering (MBSE) for Digital Avionics applications is ensuring that the system model and design/implementation remain “in-sync” during product development. We are creating a revolutionary MBSE environment that allows non-specialist developers to specify models in the SysML v2 systems modeling language, automatically generate skeletal implementations of those models in a memory-safe language (MSL), specifically Rust, as well as state and prove formal properties about the system model that can be refined and reproved against the generated design. These systems can be selected to be hosted on either Linux or the verified seL4 microkernel, or simulated using a Java Virtual Machine (JVM) based environment. In this paper, we will present our SysML v2-based toolchain, demonstrate its code generation capability on a simple digital avionics system example, and demonstrate its automatic property specification and proof capability, all in the context of an industrial Continuous Integration/Continuous Deployment (CI/CD) framework.