HAMR System Testing on seL4 -- Overview

This chapter provides an overview of system testing in HAMR: tests that run a whole composed system – the real Rust application code of every thread, on seL4, under the production schedule – and that a developer drives step by step to inject inputs, observe results, and check them. While the tests run, HAMR also checks every thread dispatch against the executable form of the model’s GUMBO component contracts and system-level properties, so a test catches contract violations it did not explicitly look for.

The current state of the tool is a “usable prototype”. It is enabled with an experimental code generation option, runs on the QEMU simulator through a command-line driver, and has a few limitations listed in §12.

The worked example throughout this chapter is the event-data-port variant of the Simple Isolette (P-EDP) from the HAMR tutorials repository, the same system whose Thermostat the GUMBOX, property-based testing, and Verus chapters use. It has all three kinds of port – data, event, and event data – and GUMBO contracts and state variables on its threads. Its system tests are in the HAMR-SysMLv2-Rust-seL4-P-EDP-Example-add-SysTest-solution project, which also adds a small composition with two system-level properties to the model (§8.1); every test and every line of test output below is quoted from that project and its runs.

We assume you have read the Manual Unit Testing chapter (the component-level testing idiom that system tests mirror), the GUMBO Component Contracts chapter (in particular its P-EDP section, whose contracts appear below), and the Manual GUMBOX Testing and Property-Based Testing chapters (executable contracts as test oracles, and PropTest). The GUMBO System-Level Properties chapter explains the composition notation used in §8.1. The Microkit Folder Structure page describes the generated project layout this chapter extends.

1. What system testing is (and why)

HAMR’s other assurance techniques each look at part of the picture:

System property verification deliberately never looks at application code: it proves properties from the contracts. Unit tests and component proofs look at code, but one component at a time, on the host. System testing is the place where the actual implementations run together, on the actual platform, in the actual schedule – so it catches what falls between those techniques: a component that is not yet verified, a contract that is weaker than the developer thought, a scenario that spans several hyperperiods, or an integration fault no single component’s contract describes.

The idea is not new to HAMR. On the JVM platform, HAMR provides a static scheduler with a command API (art.scheduling.static) for stepping through the schedule slot by slot or hyperperiod by hyperperiod, inspecting and injecting system state, and observing the results; HAMR’s JVM system testing framework is built on it (see the HAMR system testing case studies). This chapter describes the counterpart for seL4 Microkit systems written in Rust, whose commands mirror the JVM ones.

A system test is written in Rust, in the same shape as a component test:

// A reported temperature below the lower set point: the Thermostat
// commands heat, sends the command (it changed), and the Heat Source
// latches it.
fn too_cold_turns_the_heater_on() {
  set_up(Scenario {
    current_temp: 96, temp_changed: true, set_point_msg: None,
    latched: set_points(98, 101), cmd: On_Off::Off,
  });

  let _ = api::sstep(1); // thermostat
  sys_assert_eq!(last_cmd(), Some(On_Off::Onn));
  sys_assert_eq!(heat_cmd_sent(), Some(On_Off::Onn));

  let _ = api::sstep(1); // heat_source
  sys_assert_eq!(heater_state(), Some(On_Off::Onn));
}

It steps the schedule (api::), injects and inspects ports and GUMBO state variables (inspect::), asserts on what it sees, and, when it needs to, controls contract checking (observe::). The sections below take these in turn.

2. Why system testing needs the MCS user-land scheduler

HAMR generates seL4 Microkit systems under one of two scheduling models, selected by codegen’s --scheduling option (the Installation chapter describes the tools each needs):

• Domain scheduling (the default). The seL4 kernel itself runs a fixed cyclic schedule of domains, described in microkit.schedule.xml; each thread is placed in its own domain, and a small pacer protection domain dispatches it when its domain’s slot begins. The kernel switches domains on its own timer.
• MCS user-land scheduling (--scheduling UserLand). The threads’ protection domains are passive, and an ordinary user-level scheduler protection domain dispatches each one in turn by notifying it, timed by the sDDF timer driver. The system description is produced by a Python program (meta.py) rather than written as XML.

Both run the same static schedule. The difference that matters here is who is in control of it. Under domain scheduling the schedule is enforced by the kernel: nothing a test could write can pause it after one slot, hold it while a value is injected, or ask it to run “until thread X is next”. Under user-land scheduling the schedule is a user-level program, so HAMR can generate a second scheduler – the test scheduler – that waits for commands instead of a timer. System testing is therefore available only for MCS user-land builds.

The other chapters in this documentation use domain-scheduled examples, and nothing they show would change under MCS. Generating the P-EDP Isolette both ways with the same version of HAMR produces byte-for-byte identical Rust crates – application code, unit tests, GUMBOX harnesses, Verus contracts, and the system-property proof crate. What differs is only the infrastructure underneath them:

Unit tests, GUMBOX tests, and Verus run on the host and never involve the scheduler at all, which is why the earlier chapters could use either model. To keep the existing tutorials unchanged, the solution project carries both builds side by side: hamr/microkit (domain scheduling, as in the other chapters) and hamr/microkit_mcs (user-land scheduling, used here). Each tree has its own copy of the application code; the copies are identical. (Turning system testing on adds one thing to the MCS crates: threads with GUMBO state variables get a small hook through which a test can inject their values – see §4.)

3. How it works

When system testing is enabled, codegen adds a test variant of the MCS build alongside the normal image. The test variant replaces the scheduler with the test scheduler and adds one more protection domain, the test controller, which runs your tests:

┌──────────────────┐     command      ┌──────────────────┐  dispatch  ┌────────────────────┐
│ Test controller  │─────────────────▶│  Test scheduler  │───────────▶│ operator_interface │
│ (runs tests.rs)  │◀─────────────────│                  │◀───────────│ temp_sensor        │
└──────────────────┘  status, parked  └──────────────────┘  completed │ thermostat         │
         │                                                            │ heat_source        │
         │                                                            └────────────────────┘
         │   reads and writes the threads' port and state-variable memory    ▲
         └───────────────────────────────────────────────────────────────────┘

• The controller sends a command – “step one slot”, “run until thermostat_thermostat is next”, “finish this hyperperiod” – and the test scheduler dispatches threads, in the production schedule order, until the command is complete. Each thread tells the scheduler when its dispatch has finished, so stepping runs as fast as the threads do rather than waiting out each slot’s time budget. A watchdog still bounds each slot: a thread that does not finish in time fails the test that was running.
• Between commands the schedule is paused: no thread runs, and the controller can read and write the memory regions the threads communicate through – their ports and their GUMBO state variables – without racing them.
• The controller is the lowest-priority protection domain and owns no slot of the schedule, so the schedule under test is the production schedule, slot for slot.

The production image is not changed. The normal image (plain make) contains no controller and no test scheduler; the test variant is a separate image built with make CONFIG=test_scheduler.mk, and the test driver (§9) builds it for you. A tests.rs that does not compile cannot break the production build.

4. Turning it on, and what codegen generates

System testing is requested with an experimental codegen option on an MCS build:

--platform Microkit --scheduling UserLand --experimental-options ENABLE_TEST_SCHEDULER

In the tutorial projects, run it through the project’s run-hamr.cmd from the model directory, pointing --sel4-output-dir at the MCS tree (the script adds the project’s other options – source path, output directory, package name):

cd sysmlv2/isolette-simple
../bin/run-hamr.cmd --platform Microkit --scheduling UserLand \
    --experimental-options ENABLE_TEST_SCHEDULER --sel4-output-dir ../../hamr/microkit_mcs

(--runtime-monitoring is not needed for system testing, but it does no harm: it adds HAMR’s runtime-monitor variants beside the test variant.)

Beyond the normal MCS build, codegen generates:

hamr/microkit_mcs/
  test_scheduler.meta.py          # the test variant's system description
  test_scheduler.mk               # selected by: make CONFIG=test_scheduler.mk
  scheduler/src/test_scheduler.scheduler.c
  scheduler/include/test_scheduler.*.h
  bin/run-tests.cmd               # the host-side test driver (§9)
  crates/
    observers/                    # the executable contract checks (§8)
    test_controller/
      src/system_tests/
        api.rs                    # stepping commands
        inspect.rs                # get_/put_/set_/clear_ accessors for this model's ports and state variables
        observe.rs                # contract-check control: expect, take, switches
        harness.rs                # the runner, system_tests!, sys_assert!, run_property
        selection.rs, mod.rs
        tests.rs                  # YOUR TESTS -- written once, never overwritten

Everything in the controller crate is regenerated on every codegen run except tests.rs, which codegen writes once, with two small smoke tests and a commented overview of the API, and then preserves – the same arrangement as a component crate’s src/test/tests.rs.

The generated smoke tests check the test machinery itself, not the model:

system_tests! {
  suite smoke {
    fn schedule_advances_by_hyperperiod() {
      let before = api::info_state();
      let after = api::hstep(1);
      sys_assert!(after.flags & api::FLAG_BAD_COMMAND == 0);
      sys_assert_eq!(after.hyperperiod_num, before.hyperperiod_num + 1);
    }

    fn stepping_one_slot_at_a_time_wraps() {
      let n = api::schedule().num_timeslices;
      let before = api::info_state();
      let mut i = 0;
      while i < n {
        let _ = api::sstep(1);
        i += 1;
      }
      let after = api::info_state();
      sys_assert_eq!(after.current_timeslice, before.current_timeslice);
      sys_assert_eq!(after.hyperperiod_num, before.hyperperiod_num + 1);
    }
  }
}

The first asks the scheduler for one hyperperiod and checks that the command was accepted and the hyperperiod count advanced by exactly one; the second steps through the schedule one slot at a time and checks that it arrives back at the same slot one hyperperiod later. Because they use only api::, they compile for every model, so a freshly generated project has tests that run before you have written any. A passing run of them confirms the whole path: the test image builds, every thread initializes on seL4 (init=ok), the controller can drive the scheduler, and every dispatch completes within its slot’s watchdog. They also exercise the contract checks of §8, since every slot they step through is a checked dispatch – though only on whatever the system happens to do in those hyperperiods (§10). Keep them, or replace them with tests of your own; codegen does not write them again.

For Rust threads with GUMBO state variables, codegen also adds a few accessors to the thread’s bridge code so that a test can inject a state variable’s value; these are inert in the normal image.

5. Writing a system test

5.1 Declaring tests

Tests are declared inside one system_tests! block in tests.rs, grouped into suites:

system_tests! {
  suite smoke { ... }
  suite control {
    fn too_cold_turns_the_heater_on() { ... }
    fn no_event_no_command() { ... }
    fn set_point_message_triggers_and_is_latched() { ... }
    fn in_range_keeps_the_heater_as_it_is() { ... }
  }
  suite properties {
    fn heater_follows_the_control_law() { ... }
  }
  suite robustness { ... }
}

Each test is registered under its qualified name (control::no_event_no_command), which is also what the test filter matches (§9). A larger collection can be split across files: replace the block in tests.rs with system_test_files! { mod nominal_tests; mod fault_tests; } and give each file under system_tests/tests/ its own system_tests! block. Keep the _tests.rs suffix, which the model’s clean script preserves.

Why a macro rather than #[test]? The controller is a no_std program running on seL4, where cargo test’s test collection does not exist; the macro builds the table of tests that the generated runner walks.

5.2 Stepping the schedule: api::

Threads are named for run_to_thread by generated constants, one per thread: inspect::channels::thermostat_thermostat_MON. A target outside these limits – a slot index past the end of the schedule, a hyperperiod already passed, a channel that is not in the schedule – is rejected by the scheduler, which fails the test. Every command returns the scheduler’s status (hyperperiod_num, current_timeslice, …), and a command that fails – a thread overran its slot, or the target was unreachable – fails the running test automatically; that is why the examples can discard the result with let _ =.

The Isolette’s MCS schedule is one slot per thread, followed by a padding slot that fills out the one-second frame:

slot:   0                   1            2           3            4
        operator_interface  temp_sensor  thermostat  heat_source  (pad)

5.3 Observing and injecting: inspect::

For every port and GUMBO state variable, inspect.rs provides a getter and a setter named after the thread that owns the memory:

// the Thermostat's output port heat_control: Option<On_Off>
inspect::get_thermostat_thermostat_heat_control()
// the Heat Source's GUMBO state variable heater_state
inspect::get_heat_source_heat_source_sv_heater_state()
// write the Temp Sensor's output port current_temp
inspect::put_temp_sensor_temp_sensor_current_temp(t)

A getter is not a snapshot: it returns the next value the test has not yet read, and None when there is none – so reading the same port twice, with nothing written in between, gives None the second time, even for a data port that still holds its value. Reading consumes only for the test: it never takes a value from the component, or from the contract checks of §8, which read through cursors of their own. Read each value once, after the step that produces it. A port with a producer is stored in its producer’s output region, so writing it means acting as the producer: put_temp_sensor_temp_sensor_current_temp makes every consumer of that output receive the injected temperature.

For setting up a thread’s inputs, use the generated pre-state containers instead: one struct per thread holding every input port and every GUMBO state variable of that thread, and a set_<thread> function that writes them all:

pub struct thermostat_thermostat_PreState {
  pub current_temp: Isolette_Data_Model::Temp,
  pub temp_changed: Option<u8>,
  pub desired_temp: Option<Isolette_Data_Model::Set_Points>,
  pub sv_currentSetPoints: Isolette_Data_Model::Set_Points,
  pub sv_lastCmd: Isolette_Data_Model::On_Off,
}

pub struct heat_source_heat_source_PreState {
  pub heat_control: Option<Isolette_Data_Model::On_Off>,
  pub sv_heater_state: Isolette_Data_Model::On_Off,
}

Fields are named as the consuming thread sees them; state variables carry an sv_ prefix. The data input current_temp and the state variables are plain values; the event input temp_changed and the event data input desired_temp are Options, where None means nothing is pending (§6.1). (A pure event port has no payload; its field’s u8 is a placeholder, and any value means “an event”.) The containers deliberately have no Default: a Rust struct literal must name every field, so the compiler – not the developer’s vigilance – guarantees that a test’s setup is complete, and adding a state variable to the model later breaks every test that has not accounted for it (see §6).

When to inject. A producer that runs after your injection overwrites it. So inject after the producer has run and before the consumer runs: park with run_to_thread(<consumer>), set, then step. Every test starts at slot 0 of a hyperperiod (§6), so run_to_thread(thermostat) stops after the Operator Interface and the Temp Sensor have run and before the Thermostat reads their outputs. The Isolette tests describe what the Thermostat should see as a Scenario, and one helper sets it up:

/// What the Thermostat sees at its next dispatch.
struct Scenario {
  /// the sensed temperature (data port)
  current_temp: i32,
  /// whether the Temp Sensor reported a change (event port)
  temp_changed: bool,
  /// a pending set point message, if any (event data port)
  set_point_msg: Option<Set_Points>,
  /// the Thermostat's latched set points (GUMBO state variable)
  latched: Set_Points,
  /// the commanded heat state (GUMBO state variable); the heater starts in
  /// agreement with it
  cmd: On_Off,
}

/// Sets up the Thermostat and the Heat Source for scenario `s`, and parks
/// before the Thermostat in the frame where it happens.
///
/// It takes two frames.  An injected state variable takes effect when its
/// thread next runs, so injecting `lastCmd` and `heater_state` in one frame
/// would leave the two disagreeing between the Thermostat's dispatch and the
/// Heat Source's -- a real Heater_Agreement violation, of the test's own
/// making.  So the first frame puts both threads' state in place with no
/// events pending and the system assertions switched off, and the second
/// applies the scenario's events with the state already in agreement.
fn set_up(s: Scenario) {
  observe::set_sysverif(false);
  let _ = api::run_to_thread(channels::thermostat_thermostat_MON);
  set_inputs(&s, false);
  let _ = api::hstep(1);
  observe::set_sysverif(true);

  let _ = api::run_to_thread(channels::thermostat_thermostat_MON);
  set_inputs(&s, true);
}

/// Sets every input and state variable of the Thermostat and the Heat
/// Source; with `events` false, nothing is pending for either.
fn set_inputs(s: &Scenario, events: bool) {
  inspect::set_thermostat_thermostat(inspect::thermostat_thermostat_PreState {
    current_temp: temp(s.current_temp),
    temp_changed: if events && s.temp_changed { Some(0) } else { None },
    desired_temp: if events { s.set_point_msg } else { None },
    sv_currentSetPoints: s.latched,
    sv_lastCmd: s.cmd,
  });
  inspect::set_heat_source_heat_source(
    inspect::heat_source_heat_source_PreState {
      heat_control: None,
      sv_heater_state: s.cmd,
    });
}

The system assertions of §8 see each thread’s state as of its last dispatch, so state that a system property relates across threads – here lastCmd and heater_state, which Heater_Agreement (§8.1) says always agree – is best established a frame ahead, with the system checks switched off for that frame (§8.4).

5.4 Asserting: sys_assert!

Tests assert with sys_assert!(cond) and sys_assert_eq!(a, b), not assert!. A failing sys_assert* records the failure (with file, line, and condition), and returns from the test, and the runner continues with the next test. A panic would instead take the controller’s protection domain down and end the whole run.

The generated accessor names are long, so the Isolette tests wrap the four they read most in short helpers:

fn last_cmd() -> Option<On_Off> {
  inspect::get_thermostat_thermostat_sv_lastCmd()
}

fn latched_set_points() -> Option<Set_Points> {
  inspect::get_thermostat_thermostat_sv_currentSetPoints()
}

fn heat_cmd_sent() -> Option<On_Off> {
  inspect::get_thermostat_thermostat_heat_control()
}

fn heater_state() -> Option<On_Off> {
  inspect::get_heat_source_heat_source_sv_heater_state()
}

The test in §1 checks each thread’s output right after it runs, stepping one slot at a time. A test need not step slot by slot; this one runs to the end of the frame and checks only the results:

// In range, triggered: the command does not change, so no message is
// sent, and the heater keeps its state.
fn in_range_keeps_the_heater_as_it_is() {
  set_up(Scenario {
    current_temp: 99, temp_changed: true, set_point_msg: None,
    latched: set_points(98, 101), cmd: On_Off::Onn,
  });
  let _ = api::hstep(1);
  sys_assert_eq!(heat_cmd_sent(), None);
  sys_assert_eq!(heater_state(), Some(On_Off::Onn));
}

6. Test isolation: set every input

Each thread’s initialize entry point runs once, when the system boots; there is no way to return the system to its boot state between tests. So instead of resetting, system tests follow a discipline:

• Tests must be order-independent and establish their own preconditions. Whatever the previous test left in a port or state variable is what this test starts with.
• Set every input you depend on, not just the one you vary – otherwise the test silently inherits the previous test’s value. The pre-state containers (§5.3) make this checkable by the compiler.
• The runner normalizes the schedule position: before each test it advances to slot 0 of a fresh hyperperiod, so hstep(1) or run_to_thread(..) means the same thing in every test.

These rules are also what make it sound to run any subset of the tests (§9).

6.1 Event inputs: what is pending

A data port always holds one value, so “set every input” just means writing it. An event or event data input is different: what matters is whether an event is pending for the thread when it is next dispatched – and the Isolette’s other threads keep sending. The Temp Sensor signals temp_changed whenever its simulated temperature moves, and the Operator Interface sends new set points from time to time; an event the Thermostat has not taken also survives the runner’s normalization between tests. Without a way to say “nothing pending”, a test would see whatever the simulation happened to send.

So in the pre-state containers every event and event data input is an Option:

• Some(v) – exactly v is pending for the thread at its next dispatch, whatever its producer sent;
• None – nothing is pending, even if its producer sent something earlier in the frame.

The test of the Thermostat’s frame condition relies on None: with neither a temperature change nor a set point message pending, the Thermostat must not react, even to a temperature below its set points:

// The same cold temperature, but no event: the Temp Sensor reported no
// change and no set point message is pending, so the Thermostat is not
// triggered.  Nothing changes and, send-on-change, nothing is sent.
fn no_event_no_command() {
  set_up(Scenario {
    current_temp: 96, temp_changed: false, set_point_msg: None,
    latched: set_points(98, 101), cmd: On_Off::Off,
  });

  let _ = api::sstep(1); // thermostat
  sys_assert_eq!(last_cmd(), Some(On_Off::Off));
  sys_assert_eq!(heat_cmd_sent(), None);

  let _ = api::sstep(1); // heat_source
  sys_assert_eq!(heater_state(), Some(On_Off::Off));
}

Some with a set point message tests the other trigger – the message is latched, then the control law runs against it:

// A new set point message also triggers the Thermostat, and is latched
// first: 100 is in range for the old set points but above the new ones,
// so the heater goes off.
fn set_point_message_triggers_and_is_latched() {
  set_up(Scenario {
    current_temp: 100, temp_changed: false,
    set_point_msg: Some(set_points(96, 99)),
    latched: set_points(98, 101), cmd: On_Off::Onn,
  });

  let _ = api::sstep(1); // thermostat
  sys_assert_eq!(latched_set_points(), Some(set_points(96, 99)));
  sys_assert_eq!(heat_cmd_sent(), Some(On_Off::Off));

  let _ = api::sstep(1); // heat_source
  sys_assert_eq!(heater_state(), Some(On_Off::Off));
}

Outside a container, inspect::clear_<thread>_<port>() discards everything pending for one thread on one port. A clear takes effect at the start of the thread’s next dispatch, before it reads any port, and it discards only what was sent before the clear: an event sent later still arrives. That is why set_inputs can give the Heat Source heat_control: None while parked before the Thermostat – it discards stale commands, and the command the Thermostat then sends still reaches the Heat Source. §8.2 uses clear_ twice, once to tidy up after a test and once to simulate a lost message.

Two more rules matter when an output fans out to several consumers (none does in the Isolette; the SystemTesting model in HAMR’s code generator tests, hamr/codegen/jvm/src/test/resources/models/SystemTesting in the Sireum repository, has examples of each):

• Clears are per consumer; values are per output. None for one consumer leaves what is pending for the others. But the consumers of one output receive the same events, so a Some(v) sets the output for every consumer given Some, and giving two consumers of one output different Some values fails the test with setup conflict on <connection>: ...; the consumers of one connection receive the same events.
• Setters work in batches: the setter calls between two scheduler commands. Within a batch their order does not matter. A batch ends at any api:: command (even one that dispatches nothing, such as info_state()), at the start of each test, and at an explicit put_ on that output, which is a deliberate send that every consumer receives. So set up all the consumers of an output between the same two commands.

The contract checks follow a clear: a cleared event is not counted in that thread’s GUMBO checks. For the system layer, see the note on input and output aliases in §8.1.

7. Property-based system tests

System tests can draw their inputs at random, like the component-level property-based tests. The controller crate includes PropTest, built to run on seL4, and the runner provides run_property(cases, make_strategy, property): it builds the strategy, runs cases random cases, shrinks a failing case to a minimal input, and returns whether every case passed. Each case drives the real system – set up, step, observe – exactly as a fixed-value test does. A case fails only through its own prop_assert!s: a contract violation during a case (§8) fails the enclosing test, but the case itself still passes, so PropTest does not shrink toward it. To have violations drive shrinking, call observe::take() at the end of the case and prop_assert! that it holds no violation of the kind you care about.

The Isolette’s property test draws random scenarios within the Thermostat’s assumptions – temperatures it accepts, well-formed set points, any combination of events and commanded state – and checks that after the frame both the commanded state and the heater match the control law:

/// The Thermostat's control law: the command it should end up with.
fn expected_cmd(s: &Scenario) -> On_Off {
  let latched = match s.set_point_msg { Some(m) => m, None => s.latched };
  if !(s.temp_changed || s.set_point_msg.is_some()) {
    s.cmd
  } else if s.current_temp > latched.upper.degrees {
    On_Off::Off
  } else if s.current_temp < latched.lower.degrees {
    On_Off::Onn
  } else {
    s.cmd
  }
}

// Random scenarios within the Thermostat's assumptions: temperatures the
// Temp Sensor can report to it, well-formed set points, and any
// combination of events.  After the frame the heater holds the command
// the control law selects.  The system assertions (Heater_Agreement,
// Too_Cold_Heats) are checked on every case as well.
fn heater_follows_the_control_law() {
  sys_assert!(run_property(32, || any_scenario(), |s| {
    let expected = expected_cmd(&s);
    set_up(s);
    let _ = api::hstep(1);
    proptest::prop_assert_eq!(last_cmd(), Some(expected));
    proptest::prop_assert_eq!(heater_state(), Some(expected));
    Ok(())
  }));
}

/// Random scenarios within the Thermostat's assumptions: temperatures it
/// accepts (95..104), well-formed set points (at most 5 apart), any
/// combination of events, and either commanded state.
fn any_scenario() -> impl Strategy<Value = Scenario> {
  let temps = 95i32..=104;
  let events = (proptest::bool::ANY, proptest::bool::ANY);
  let span = (95i32..=104, 0i32..=5);
  let cmd = proptest::prop_oneof![Just(On_Off::Onn), Just(On_Off::Off)];
  (temps, events, span.clone(), span, cmd).prop_map(
    |(t, (changed, msg), (lo, w), (mlo, mw), cmd)| Scenario {
      current_temp: t,
      temp_changed: changed,
      set_point_msg: if msg { Some(set_points(mlo, mlo + mw)) } else { None },
      latched: set_points(lo, lo + w),
      cmd,
    })
}

/// How a shrunk failing scenario is printed:
/// `temp 102, no change, msg 95..95, latched 95..95, cmd Onn`.
impl core::fmt::Debug for Scenario {
  fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
    let change = if self.temp_changed { "change" } else { "no change" };
    write!(f, "temp {}, {}, msg ", self.current_temp, change)?;
    match self.set_point_msg {
      Some(m) => write!(f, "{}..{}", m.lower.degrees, m.upper.degrees)?,
      None => write!(f, "none")?,
    }
    write!(f, ", latched {}..{}, cmd {:?}",
           self.latched.lower.degrees, self.latched.upper.degrees, self.cmd)
  }
}

The component-level property tests check the Thermostat’s contract on random inputs; this test checks that the composed system – Thermostat, Heat Source, and the event data connection between them – delivers the control law end to end, while the system-level properties of §8.1 are checked on every case.

run_property takes a function that builds the strategy (|| ...), not the strategy itself. The controller has no operating system, so its heap is a fixed region that run_property sets up the first time it runs. Building a strategy can allocate (prop_flat_map, .boxed(), and prop_oneof! – as in any_scenario above – all do), and an argument expression would be evaluated before run_property had set up the heap. Passing a closure defers building the strategy until the heap exists.

Seeds and reproducing a failure. There is no source of randomness on the target, so the cases are determined by a seed, PROPTEST_SEED, built into the test image. The test driver picks a fresh seed for every run, so each run explores new cases, and prints it:

TEST | INFO  32 generated cases passed (PROPTEST_SEED=30c3b5124b93ebd5cd1de5beab1f2b8762defc8e15fb379a1b69d4c158a10f6c)

A failure prints the shrunk input and the seed to pass back to reproduce the run (PROPTEST_SEED=<seed> bin/run-tests.cmd); §10 shows one. Cases share the running system, just as tests do, so each case must set what it depends on – here, set_up does.

8. Contract checking during tests

Assertions in a test check what the test author thought to check. In addition, while the tests run, the controller checks every dispatch of every thread against the executable forms of the model’s specifications:

• the GUMBO layer – each thread’s component contracts: its initialize guarantees (once, at boot), and at every dispatch its compute assumptions and integration assumptions (CEP_Pre) and its compute guarantees and integration guarantees (CEP_Post). These are the same GUMBOX predicates the component test harnesses use;
• the system layer – for each composition in the model, every place assertion of every concrete property, checked as the schedule passes that place.

Both layers are generated whenever the model has the corresponding specifications, and both are on by default. A violation during a test’s body fails that test, even if the test asserted nothing about it. A broken initialize guarantee, checked at boot before any test runs, fails the run as a whole (DONE ... init=failed). Violations while the runner moves the schedule back to slot 0 between tests are tracked but not reported: they belong to no test. A violation is reported as a VIOLATION line naming the contract and where the schedule was, followed for a GUMBO contract by the values it was checked on:

TEST | VIOLATION CEP_Post heat_source_heat_source hp=7 slot=3
TEST | INFO  heat_source_heat_source pre: PreState_heat_source_heat_source { In_heater_state: Onn, api_heat_control: Some(Off) }
TEST | INFO  heat_source_heat_source post: PostState_heat_source_heat_source { heater_state: Onn }
TEST | VIOLATION SysAssert nominal/Heater_Agreement at after hs hp=7 slot=3

A test controls this checking through a third generated module, observe:: (observe.rs, generated when the model has contracts), alongside api:: and inspect::. It hosts the two layers – reading the threads’ ports and state variables at every dispatch, running the checks, and recording each violation against the running test – and gives the test a say in what becomes of a violation:

8.1 The example’s system properties

The P-EDP Isolette has no system-level properties of its own, so the solution project adds a composition to the top-level system (sysmlv2/isolette-simple/Isolette.sysml). It states one thing neither component contract says on its own. The Thermostat sends a heat command only when its commanded state lastCmd changes (send-on-change), and the Heat Source latches each command it receives into heater_state. Together they keep the two equal: both start Off, a change is sent and latched in the same frame, and no change means no message and nothing to latch.

composition nominal {
  components
    oi     = operator_interface.operator_interface;
    sensor = temp_sensor.temp_sensor;
    therm  = thermostat.thermostat;
    hs     = heat_source.heat_source;

  // The temperature and the change event are the Thermostat's inputs: what it
  // received, which is what its control law reacts to.
  ports
    sensedTemp  = therm.current_temp;    // data port
    tempChanged = therm.temp_changed;    // event port
    heatCmd     = therm.heat_control;    // event data port (output)

  state
    lastCmd     = therm.lastCmd;
    setPoints   = therm.currentSetPoints;
    heaterState = hs.heater_state;

  schema { oi; sensor; therm; hs }

  abstract property Heater_Agreement_Base ... {
    at START ...:     (heaterState == lastCmd) & (setPoints.lower.degrees <= setPoints.upper.degrees);
    ...
    after therm "send-on-change: either the new command is on its way, or the
      |command did not change and the heater already agrees with it":
      ((HasEvent(heatCmd) and heatCmd == lastCmd) or
       ((not HasEvent(heatCmd)) and heaterState == lastCmd)) &
      (setPoints.lower.degrees <= setPoints.upper.degrees);
    after hs ...:     (heaterState == lastCmd) & (setPoints.lower.degrees <= setPoints.upper.degrees);
    at END ...:       (heaterState == lastCmd) & (setPoints.lower.degrees <= setPoints.upper.degrees);
  }

  property Heater_Agreement :> Heater_Agreement_Base
    "every frame, the heater's state equals the Thermostat's commanded state" {
  }

  property Too_Cold_Heats :> Heater_Agreement_Base
    "a reported temperature below the lower set point turns the heater on in
    |the same frame" {
    after therm ...:  (HasEvent(tempChanged) and sensedTemp.degrees < setPoints.lower.degrees)
                        implies lastCmd == Isolette_Data_Model::On_Off.Onn;
    after hs ...:     (HasEvent(tempChanged) and sensedTemp.degrees < setPoints.lower.degrees)
                        implies heaterState == Isolette_Data_Model::On_Off.Onn;
  }
}

(Abridged; the full text is in the solution project.) Heater_Agreement is a loop invariant; the set points’ well-formedness rides along because the Thermostat assumes it, and a property covering the Thermostat must establish its assumptions. Too_Cold_Heats builds on it: a reported change below the lower set point makes the heater On by the end of the frame. Both are verified with Verus from the component contracts, as the system properties chapter describes (make -C crates/sys_nominal_proof – 24 verification conditions); system testing then checks the same assertions at run time, against the real code.

Input or output aliases. sensedTemp and tempChanged name the Thermostat’s inputs, not the Temp Sensor’s outputs. In the proof the two are the same channel; at run time an output alias means what the producer sent in the frame, and an input alias what the consumer received – which differ when a test clears or injects an event (§6.1). A property about how a thread reacts is therefore best stated over that thread’s inputs: over the Temp Sensor’s outputs, Too_Cold_Heats would also judge frames in which a test had withheld the sensor’s event from the Thermostat.

8.2 A broken assumption rejects the dispatch

A thread’s CEP_Pre is its contract with whoever sends it data. When it does not hold, the controller reports CEP_Pre, fails the test, and rejects the dispatch: the thread’s slot passes without running it, so the out-of-contract values never reach its code. (HAMR’s runtime monitors, by contrast, only report a failed assumption.) Because the rejected thread produced nothing in that frame, the system layer suspends its assertions until the next hyperperiod, and says so. The rejected input stays pending – an event until the thread next consumes it – so a thread whose input stays out of contract is rejected at every dispatch.

8.3 Tests that cause a violation on purpose

A robustness test drives the system outside its contracts deliberately and must say which violation it expects. observe::expect(..) declares it: a matching violation is reported as INFO instead of failing the test, and the test fails if the violation does not occur. The Thermostat assumes every set point message is well-formed:

// The Thermostat assumes every set point message is well-formed
// (lower <= upper).  A malformed one fails its CEP_Pre, so the
// controller rejects the dispatch: the Thermostat does not run, and its
// state is untouched.  The message is still pending after the
// rejection, so the test clears it -- otherwise the Thermostat would be
// rejected again at every later dispatch.
fn malformed_set_point_is_rejected() {
  observe::expect(observe::Expect::CepPre(
    observe::Thread::thermostat_thermostat));
  set_up(Scenario {
    current_temp: 96, temp_changed: true,
    set_point_msg: Some(set_points(101, 98)),
    latched: set_points(98, 101), cmd: On_Off::Off,
  });
  let _ = api::sstep(1); // the thermostat's slot passes; it does not run
  sys_assert_eq!(latched_set_points(), Some(set_points(98, 101)));
  sys_assert_eq!(last_cmd(), Some(On_Off::Off));
  inspect::clear_thermostat_thermostat_desired_temp();
}

TEST | BEGIN robustness::malformed_set_point_is_rejected
TEST | INFO  expected violation: CEP_Pre thermostat_thermostat hp=75 slot=2
TEST | INFO  channel 4 not dispatched at hp=75 slot=2: its inputs did not meet its CEP_Pre; system assertions suspended until the next frame
TEST | PASS  robustness::malformed_set_point_is_rejected

Expect can name a thread’s CepPre or CepPost, or a system property: Expect::SysAssert(observe::sys::nominal::COMPOSITION, observe::sys::nominal::Heater_Agreement). A SysAssert expectation matches any violation of that property, at any of its assertion points – which can hide a second, unrelated fault that breaks the same property. When the point matters, take the violations instead with observe::take() and assert on them; violations taken this way no longer fail the test (they are still printed).

The second robustness test uses that to show a fault that only the system layer can see: it loses the heat command in transit. The Thermostat sends On, and the test clears it before the Heat Source runs, as a dropped message would. Each thread still meets its own contract – the Heat Source received nothing, so it holds its state – but the heater no longer agrees with the commanded state:

// Loses the heat command in transit: the Thermostat sends On, and the
// test clears it before the Heat Source runs, as a dropped message
// would.  Each thread still meets its own contract -- the Heat Source
// received nothing, so it holds its state -- but the heater no longer
// agrees with the commanded state, which only the system layer can see.
// The test takes the violations and checks that they are all system
// assertions, the first of them right after the Heat Source.  (The
// frame then ends, so the invariant's END and START assertions break as
// well; the next test's set_up puts the heater back in agreement.)
fn lost_command_breaks_heater_agreement() {
  set_up(Scenario {
    current_temp: 96, temp_changed: true, set_point_msg: None,
    latched: set_points(98, 101), cmd: On_Off::Off,
  });
  let _ = api::sstep(1); // thermostat sends On
  sys_assert_eq!(heat_cmd_sent(), Some(On_Off::Onn));
  inspect::clear_heat_source_heat_source_heat_control();
  let _ = api::sstep(1); // heat_source receives nothing
  sys_assert_eq!(heater_state(), Some(On_Off::Off));

  let violations = observe::take();
  let first = violations.iter().next();
  sys_assert!(violations.iter()
    .all(|v| v.kind == observe::Kind::SysAssert));
  sys_assert!(first.map_or(false, |v| v.point == "after hs"));
  sys_assert!(violations.contains(observe::Expect::SysAssert(
    observe::sys::nominal::COMPOSITION,
    observe::sys::nominal::Heater_Agreement)));
}

TEST | BEGIN robustness::lost_command_breaks_heater_agreement
TEST | INFO  system assertions resumed at hp=76
TEST | VIOLATION SysAssert nominal/Heater_Agreement at after hs hp=77 slot=3
TEST | VIOLATION SysAssert nominal/Heater_Agreement at at END hp=77 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at after hs hp=77 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at at END hp=77 slot=3
TEST | VIOLATION SysAssert nominal/Heater_Agreement at at START hp=77 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at at START hp=77 slot=3
TEST | PASS  robustness::lost_command_breaks_heater_agreement

The first violation is the one that matters – Heater_Agreement broken right after the Heat Source – and the rest follow from it: the Heat Source is the frame’s last thread, so the same disagreement is also seen at END and at the next frame’s START. The GUMBO layer reports nothing, because neither thread broke its own contract. (The first INFO line is the previous test’s rejected dispatch ending: the system layer resumes at the new hyperperiod.)

8.4 Turning checks off

Each layer can be turned off at three levels:

The runner restores the build-level setting after every test, so a test cannot leave checks off for the next one. A suite or test cannot turn on a layer that the build turned off. A layer switched off at suite or test level keeps tracking the system, so switching it back on – as set_up does after its setup frame – is immediately correct. Turning checks off is the blunt tool; for a test that trips one contract on purpose, prefer observe::expect or observe::take, which keep every other contract checked.

9. Running the tests

Requires the seL4 Microkit SDK, LionsOS, sdfgen, and qemu-system-aarch64 (see Installation). The driver uses sh and pkill to stop QEMU, so it does not run on Windows. Like HAMR’s other .cmd scripts it runs itself through Sireum, so SIREUM_HOME must be set. From the MCS tree:

cd hamr/microkit_mcs
bin/run-tests.cmd                 # every test
bin/run-tests.cmd control::       # one suite
bin/run-tests.cmd heater          # every test whose name contains "heater"
bin/run-tests.cmd --list          # list the tests; run nothing

The filter is a substring of the qualified suite::test name. run-tests.cmd builds the test image (a debug build, which it forces, since the test output is printed with debug printing), boots it under QEMU, reads the serial output, stops QEMU when the run is done, and exits with a nonzero code unless every selected test passed. The first build takes a minute or two; changing only the filter, the seed, or the check switches afterwards relinks the image in seconds. The environment variables PROPTEST_SEED, GUMBO_CHECKS, and SYSVERIF_CHECKS are passed through to the build.

The output that matters is every line beginning TEST | . The serial console is the only channel that carries results off the target, and it also carries everything else the system prints – the loader and kernel boot messages, the scheduler’s SCHEDULER | ... lines, each thread’s own logging – so the controller marks its lines with a prefix, and the driver reads only lines that start with TEST | . (Anchoring at the start of the line means a message that merely mentions DONE cannot end the run early.)

TEST | LIST  smoke::schedule_advances_by_hyperperiod
...
TEST | LIST  robustness::lost_command_breaks_heater_agreement
TEST | BEGIN smoke::schedule_advances_by_hyperperiod
TEST | PASS  smoke::schedule_advances_by_hyperperiod
...
TEST | BEGIN control::no_event_no_command
TEST | PASS  control::no_event_no_command
...
TEST | DONE  matched=9 passed=9 failed=0 init=ok
OK: 9 of 9 tests passed

• LIST lines are the table of registered tests (with (not selected) after those the filter leaves out); BEGIN, then PASS or FAIL, bracket each test; INFO and VIOLATION lines appear in between.
• A failing test prints one FAIL line naming its first failure – a sys_assert* (<file>:<line> <condition>), a failed command, or contract violation (<n> in this test) – and any further failures as INFO also failed: ....
• DONE closes the run: matched tests selected, how many passed and failed, and init=ok when every thread’s initialize guarantee held at boot.

The driver’s verdict is deliberately strict, because the typical failure of a bare-metal run is silence – a hang, a crash, a controller that never started. A run fails unless it ends with a DONE line, the filter matched at least one test (a mistyped filter fails loudly rather than passing with nothing run), the PASS/FAIL lines reconcile with the counts, and init=ok.

10. Seeing the checks catch a bug

To see what the checks contribute, seed a bug: make the Heat Source ignore Off commands. In crates/heat_source_heat_source/src/component/heat_source_heat_source_app.rs, change the line that latches a received command, self.heater_state = cmd;, to if let On_Off::Onn = cmd { self.heater_state = cmd; }, and rerun the tests. Two of the nine now fail:

TEST | BEGIN control::set_point_message_triggers_and_is_latched
TEST | VIOLATION CEP_Post heat_source_heat_source hp=7 slot=3
TEST | INFO  heat_source_heat_source pre: PreState_heat_source_heat_source { In_heater_state: Onn, api_heat_control: Some(Off) }
TEST | INFO  heat_source_heat_source post: PostState_heat_source_heat_source { heater_state: Onn }
TEST | VIOLATION SysAssert nominal/Heater_Agreement at after hs hp=7 slot=3
TEST | VIOLATION SysAssert nominal/Heater_Agreement at at END hp=7 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at after hs hp=7 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at at END hp=7 slot=3
TEST | VIOLATION SysAssert nominal/Heater_Agreement at at START hp=7 slot=3
TEST | VIOLATION SysAssert nominal/Too_Cold_Heats at at START hp=7 slot=3
TEST | FAIL  src/system_tests/tests.rs:189 heater_state() == Some(On_Off::Off)
TEST | INFO  also failed: contract violation (7 in this test)
...
TEST | BEGIN properties::heater_follows_the_control_law
...
TEST | INFO  assertion failed: `(left == right)`
TEST | INFO    left: `Some(Onn)`,
TEST | INFO   right: `Some(Off)` at src/system_tests/tests.rs:217
TEST | INFO  minimal failing input: temp 102, no change, msg 95..95, latched 95..95, cmd Onn
TEST | INFO  reproduce with PROPTEST_SEED=7e2df0edb40cc665604e2ff9c199fa9b590aab415028cdf158f70cfef495a36d
TEST | FAIL  src/system_tests/tests.rs:212 run_property(32, || any_scenario(), |s|
TEST | INFO  also failed: contract violation (105 in this test)
...
TEST | DONE  matched=9 passed=7 failed=2 init=ok
FAILED: 2 of 9 tests failed

Reading the output:

• Both layers see the bug at the same dispatch. The GUMBO layer reports the Heat Source’s own guarantee (HS_latch_cmd: a received command is latched) and the values it was checked on – an Off command arrived, and the heater stayed On. The system layer reports Heater_Agreement breaking right after the Heat Source, and everything that follows from it.
• The test’s own assertion reports what it expected (== Some(On_Off::Off)), and its contract violations follow as also failed.
• The property test shrinks its failure to a minimal scenario: temperature 102, no temperature event but a set point message 95..95, and the heat On – too hot for the new set points, so the Thermostat sends Off, which the Heat Source ignores. The printed seed reproduces the run.
• Only the tests that send an Off command fail. The smoke tests and the other scenarios pass: the contract checks judge what the system does, and in those runs no Off command was ever sent. Contract checking makes every test a check of every contract, but only on the behavior the tests drive – which is why the scenarios, and the random cases, matter.

The same bug would be found by the Heat Source’s own unit tests and by Verus. The point of the exercise is that system tests do not depend on those having been written or run: the contracts travel with the model and are checked at every dispatch of the composed system.

11. Authoring workflow and tips

1. Generate, then list. After enabling the option, run run-tests.cmd --list first: it confirms the toolchain, the build, and the boot without running anything, and shows the generated smoke tests.
2. Start from the dataflow. Decide which thread’s input you control and which outputs you observe; inject after the producer and before the consumer (run_to_thread(<consumer>)), and use the set_<thread> containers so the compiler checks that your setup is complete.
3. Say what is pending. The other threads keep running and sending; give every event input Some or None explicitly, and clean up any event your test leaves pending (§6.1).
4. Establish related state in a setup frame. When a system property relates the state of several threads, inject it a frame ahead, with the system checks off, so the threads never disagree mid-frame (§5.3).
5. Write helpers for the common moves – set_up, a Scenario struct – so each test reads as its scenario.
6. Check intermediate values while developing a test (sstep(1) and a get_), then simplify to the outputs that matter.
7. Let the contracts do the routine checking. A test’s own assertions should state the scenario’s expected result; “every thread stayed within its contract” is checked for you.
8. Name the violations you cause. Use observe::expect for a robustness test; use observe::take() when the property is checked at several places and the place matters.
9. State reactive system properties over what the reacting thread receives (§8.1), so they stay true when a test clears or injects events.
10. Keep tests short in hyperperiods. Each test runs on the real system; property tests multiply that by the number of cases. Reproduce failures with the printed PROPTEST_SEED rather than by raising the case count.

12. Current limitations

• MCS user-land scheduling only (§2), on the QEMU simulator, through a driver that does not run on Windows.
• No reset between tests. Initialization runs once at boot; tests must be order-independent and set every input (§6).
• Single-element event queues. With system testing enabled, codegen rejects a thread with GUMBO contracts that has a deeper event queue.
• Debug builds only. Test output uses the debug console; the driver forces a debug build.
• No interactive mode. Tests are compiled into the image; there is not yet a console for stepping the schedule by hand.

13. Further examples

• Simple Isolette, P-EDP – the solution project used throughout this chapter (hamr/microkit_mcs/crates/test_controller/src/system_tests/tests.rs, and the composition in sysmlv2/isolette-simple/Isolette.sysml).
• Struct Split – the solution project of the system-testing tutorial (see the Recommended Reading Order): a data-port-only pipeline whose tests follow one struct through every stage, check the saturation boundaries, run a property-based end-to-end test against the End_To_End_Functional property of the system properties chapter, and corrupt a value in transit that only the system layer detects.
• Isolette in loonwerks/INSPECTA-models (hamr/microkit_mcs) – the full Isolette, with data ports; the system tests of HAMR’s JVM Isolette case study, ported to seL4 and split across files with system_test_files!. They use GUMBO state-variable injection, a reinitialize() helper that resets every state variable a test depends on, and property-based tests.
• SystemTesting in HAMR’s code generator tests (hamr/codegen/jvm/src/test/resources/models/SystemTesting in the Sireum repository) – a small model built to exercise the test machinery itself: an event data port fanning out to two consumers, one written in C, a feedback edge, and its clearing suite of setup-batch examples.

Related

• GUMBO System-Level Properties – the composition notation of §8.1, and how system properties are verified.
• GUMBO Component Contracts – the P-EDP Thermostat and Heat Source contracts the GUMBO layer checks.
• Manual GUMBOX Testing and Property-Based Testing – the component-level counterparts of §5 and §7.
• GUMBO to GUMBOX Translation – the executable contracts the GUMBO layer evaluates.
• Installation – the MCS build dependencies (LionsOS, sdfgen) and QEMU.