Recommended Reading Order

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)

  • Video - lecture
  • Slides – slides used in the video above
  • Documentation – in large part, a transcript of the video above.

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

  • Video - lecture
  • Slides – slides used in the video above

2. Installation - install Sireum/HAMR and the IDEs and platform tools (CodeIVE, Rust/Verus, seL4 Microkit) you will need for the rest of the documentation.

• Installation

  • Documentation

• Cloning / Downloading Example Repository

  • Documentation Forthcoming

• Confirming installation

  • Documentation Forthcoming

3. Semantics Concepts — read the informal semantics of AADL modeling elements (threads, processes, ports, communication patterns) using the Simple Isolette as the running example.

• Documentation

4. 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.

• Documentation

5. 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.

• Documentation - Thread Component Application Code Development in Rust
• Documentation - Thread Component Manual Unit Testing in Rust

6. Tutorial: Refactoring an Existing System - The Simple Isolette (Part 1 - Working with SysMLv2 in the CodeIVE)

• Tutorial instructions
• Video - walkthrough of solution
• Note: Starting files and solution files are linked in tutorial description

7. Tutorial: Refactoring an Existing System - The Simple Isolette (Part 2 - Code Generation and Working with HAMR-generated Rust Code and Manual Unit Tests)

• Tutorial instructions
• Video - walkthrough of solution
• Note: Starting files and solution files are linked in tutorial description

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

9. 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.

10. 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)

• Tutorial instructions
• Link to completed models and code are provided in the tutorial text.

11. GUMBO Component Contracts — learn the GUMBO contract language for specifying component behavior and the contracts that downstream tooling will reason about

• Documentation - GUMBO Overview and Rationale
• Documentation - GUMBO Component Contracts – example-based walkthrough of contract structure
• GUMBO Quick Reference – reference “cheat sheet” of contract constructs
• GUMBO Grammar – BNF-style syntax reference (optional)

12. 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.

12. 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

• Documentation - GUMBO to GUMBOX Translation – how each contract form becomes Rust boolean functions, and how to call them directly
• Documentation - Manual GUMBOX Testing – writing contract-checked unit tests with hand-chosen inputs, judged automatically by the GUMBOX oracles
• Documentation - Automated GUMBOX Property-Based Testing – driving the same contract-checked harnesses with randomly generated test vectors from HAMR-generated value strategies

13. 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.

14. 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

• Documentation - GUMBO to Verus Translation and Verification – how each contract form becomes a Verus contract, the verification workflow, and common Verus limitations

15. 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.

16. GUMBO System Contracts — learn how to specify and verify HAMR system properties

• GUMBO System Properties Overview
• GUMBO System Properties Verification - Technical Reference for VC structure (optional)

16. Tutorial: GUMBO System Contracts with Formal Verification (Part 1 - Extending an Existing System Model with Additional System Property Specifications)

• Tutorial instructions
• Solution files - see Part 2 below

17. Tutorial: GUMBO System Contracts with Formal Verification (Part 2 - Performing System Property Verification and Working with Verification Conditions (VCs)

• Tutorial instructions
• Solution files - for Parts 1 and 2

18. HAMR System Testing — run the whole composed system on seL4 (under QEMU), stepping the schedule, injecting and inspecting port and state values, with every thread dispatch checked against the GUMBO component contracts and system properties

• Documentation - HAMR System Testing on seL4

19. Tutorial: System Testing the Struct Split Example (Part 1 - Writing and Running System Tests) — the documentation above uses the event-data-port Simple Isolette; the tutorial returns to the Struct Split example from the system-property tutorials

• Tutorial instructions
• Solution files - see Part 2 below

20. Tutorial: System Testing the Struct Split Example (Part 2 - Property-Based Tests and Contract Checking)

• Tutorial instructions
• Solution files - for Parts 1 and 2