SysML is a standardized modeling language used throughout industry for systems engineering – particularly for embedded systems. The Object Management Group (OMG) is developing a new version of SysML referred to as SysMLv2. Instead of SysML modeling concepts being shoe-horned into UML as a UML profile, SysMLv2 has been reengineered from its foundations to provide a cleaner and more rigorous presentation of system modeling concepts. It has adopted features that have been central to AADL for decades – the most notable are: (a) the inclusion of companion textual and graphical views of a model, and (b) a much greater focus on model semantics. Moreover, many AADL concepts including system component categories and port-based communication can be presented directly as SysMLv2 modeling features. Due to the anticipated widespread adoption of SysMLv2 within industry as well of commercial tooling from largest vendors of industry modeling tools, the AADL standards committee is working with OMG to determine how AADL concepts can be presented in SysMLv2.

We have developed a prototype SysMLv2 front-end for HAMR based on the open source OMG community SysMLv2 pilot implementation. Our prototype supports a subset of SysMLv2 sufficient for representing AADL models used on recent and current Department of Defense research projects including DARPA CASE and DARPA PROVERS. The prototype translates the supported SysMLv2 subset into the same intermediate representation used by HAMR to support AADL. Therefore, the prototype supports HAMR code generation for all existing HAMR-support programming languages and platform targets including Scala/Slang/JVM, and C for Linux and the seL4 microkernel. Moreover, as we add support for Rust in HAMR on DARPA PROVERS, HAMR will be able to generate Rust-based implementation for the new seL4 Microkit (previously called the “core platform”).

To illustrate these capabilities, we have ported AADL models for several systems including the Galois’ HARDENS Reactor Trip System, the “Isolette” infant incubator introduced in the FAA’s Requirements Engineering Management Handbook. For each of these, we have used HAMR to build system deployments for JVM, C/Linux, and C/seL4 platforms. As an example, see the GitHub repository for the KSU HAMR version of the Galois HARDENS Reactor Trip System.

Moving forward, we are:

  • working within the AADL Committee and partner committees within the OMG on standardizing AADL concepts in SysMLv2,
  • extending our HAMR SysMLv2 prototype capabilities as part of the DARPA PROVERS program,
  • enhancing our mechanized formal semantics of HAMR (built in the Isabelle theorem prover) to support SysMLv2 concepts that we believe would enhance our ability to support realistic embedded systems.

We are seeking additional funding to harden our HAMR SysMLv2 prototype to support industrial workflows.