This page suggests an order for working through the HAMR lecture videos, tutorials, and reference documentation. It is aimed at readers who are new to HAMR and want a guided path; experienced readers should feel free to jump directly to the reference documentation chapters most relevant to their work.

Suggested Reading Order for SysMLv2 Modeling with Rust Code Development

  1. HAMR Overview — start here to understand HAMR’s three development layers, HAMR as a formal-methods pipeline, and the kinds of systems HAMR targets.

  • HAMR Overview (Part 1 - General concepts and modeling)

  • HAMR Overview (Part 2 - Rust thread component development)

  1. Installation - install Sireum/HAMR and the IDEs and platform tools (CodeIVE, Rust/Verus, seL4 Microkit) you will need for the rest of the documentation.
  1. Semantics Concepts — read the informal semantics of AADL modeling elements (threads, processes, ports, communication patterns) using the Simple Isolette as the running example.
  1. Editing and Code Generation Using SysMLv2 Models — set up and use the VSCodium-based IDE to actually author SysMLv2 models, run the type checker, and configure code generation.
  1. Thread Component Application Code Development in Rust and Manual Unit Testing — fill in the Rust application logic for generated HAMR thread skeletons: entry points, port APIs.
  1. Tutorial: Refactoring an Existing System - The Simple Isolette (Part 1 - Working with SysMLv2 in the CodeIVE)
  1. Tutorial: Refactoring an Existing System - The Simple Isolette (Part 2 - Code Generation and Working with HAMR-generated Rust Code and Manual Unit Tests)

  1. Microkit Folder Structure — get oriented to the folder layout that HAMR generates for seL4 Microkit projects with Rust components.

  2. Tutorial: Building a HAMR System From Scratch - The Simple Network Guard (Part 1 - Working with SysMLv2 in the CodeIVE)

  • Tutorial instructions
  • Completed models and code for Parts 1 and 2 can be found at the conclusion of Part 2 of the tutorial below.
  1. Tutorial: Building a HAMR System From Scratch - The Simple Network Guard (Part 2 - Code Generation and Working with HAMR-generated Rust Code and Manual Unit Tests)
  1. GUMBO Component Contracts — learn the GUMBO contract language for specifying component behavior and the contracts that downstream tooling will reason about
  1. Tutorial: Adding GUMBO Thread Component Contracts to an Existing System - The Simple Isolette System (Part 1 - Adding GUMBO Thread Contracts to SysMLv2 Models)
  • Tutorial instructions
  • Completed models and code for Parts 1, 2, and 3 can be found at the conclusion of Part 3 of the tutorial below.
  1. GUMBOX Rust Executable Contracts and Manual GUMBOX Testing — learn how HAMR translates GUMBO thread contracts to executable Rust boolean functions that can be used for both testing and run-time monitoring
  1. Tutorial: Adding GUMBO Thread Component Contracts to an Existing System - The Simple Isolette System (Part 2 - GUMBOX executable Rust contracts and Manual GUMBOX Testing)
  • Tutorial instructions
  • Completed models and code for Parts 1, 2, and 3 can be found at the conclusion of Part 3 of the tutorial below.
  1. HAMR Translation of GUMBO Contracts to Verus Contracts and Verus Formal Verification — learn how HAMR translates GUMBO thread contracts to Verus Rust code contracts to support formal verification of HAMR thread component application code
  1. Tutorial: Adding GUMBO Thread Component Contracts to an Existing System (Part 3 - Verus Contracts and Verus Formal Verification of Rust thread component code)
  • Tutorial instructions
  • Completed models and code for Parts 1, 2, and 3 can be found in the tutorial text.