This repository provides tutorials and small examples for the HAMR high-assurance model-driven development environment (HAMR web site).
-
Tutorial: Modifying an Existing HAMR SysMLv2/Rust system (working with the Simple Isolette example)
- Part 1: Modifying an existing HAMR SysMLv2 model (adding a Display Temperature feature to the Simple Isolette model)
- Part 2: Re-running Code Generation and Modifying existing HAMR Rust Components and Tests (adding code and tests for the Display Temperature feature)
-
Tutorial: Building a simple HAMR SysMLv2/Rust system from scratch (building the Simple Netword Guard example)
-
Tutorial: Working with GUMBO Contracts in the Simple Isolette Example (writing contracts, testing using GUMBOX executable contracts, formally verifying Rust component application code to contracts using Verus)
- Part 1: Modifying an existing HAMR SysMLv2 model (adding a Display Temperature feature to