|
This repository supports the exploration and development of SysMLv2-based representations of AADL models (SysMLv2/AADL). It provides library definitions for AADL concepts, developed by the Real-Time Embedded Safety-Critical (RTESC) working group, along with example SysMLv2 models that demonstrate how these definitions can be applied in practice.
Visit the Sireum Getting Started page. In the section Both VSCodium-based and Intellij-based IVEs, run the script that is appropriate for your platform. This will install:
-
Sireum: A research platform for developing high-assurance systems. It includes HAMR (High-Assurance Modeling and Rapid engineering), which translates SysMLv2 and AADL models into AIR (an intermediate representation) and performs semantic analysis and code generation targeting safety-critical platforms.
-
CodeIVE: A fully configured VS Code environment with Sireum/HAMR extensions and SysIDE, which provides editing, validation, and navigation support for SysMLv2/AADL models.
-
IVE (Integrated Verification Environment): An IntelliJ-based IDE tailored for working with Slang, Sireum’s modeling and programming language. Slang supports formal contracts, which can be verified using the Logika verification engine to reason about functional correctness through contracts and proofs.
After installation, you can open and edit the example models in CodeIVE, validate them against the RTESC SysMLv2 library definitions, and perform downstream processing such as code generation using HAMR. Each example model in this repository includes its own set of instructions to guide you through validation, analysis, and tool usage.
-
SysMLv2/AADL Quick Syntax Guide
A concise summary of how AADL concepts are expressed using SysMLv2 and the RTESC definitions.
Isolette model and well-formedness checking in the HAMR (SysIDE) VSCode extension for SysMLv2
Isolette model-level GUMBO integration constraint checking with error reporting in VSCode
Isolette HAMR code generation for JVM and seL4 microkit
Isolette HAMR Rust code development, verification, testing, and deployment on seL4