MAPE-K Simulation Guide

MIRR includes a deterministic MAPE-K autonomic simulator that validates whether hardware monitors can observe and respond to runtime anomalies. Unlike purely static verification, the simulator exercises temporal properties under fault injection, closing the loop between design-time specification and runtime adaptation.

Table of Contents

1. What is MAPE-K?
2. Architecture
3. The five components
4. Bounded LTL properties
5. Signal predicates
6. Adaptation actions
7. The neonatal monitoring scenario
8. API entry points
9. Bounded iteration guarantees
10. Knowledge base and audit trail

What is MAPE-K?

MAPE-K is the canonical framework for self-adaptive systems, first described by Kephart and Chess (2003). The acronym stands for:

• Monitor -- observe the system via sensors
• Analyze -- evaluate temporal properties over observed data
• Plan -- select the best corrective action
• Execute -- apply the selected action to the system
• Knowledge -- shared audit log of all decisions

These five phases execute in strict sequence on every simulation tick, forming a feedback loop. The knowledge base is shared across all phases, enabling post-run analysis and auditability.

The implementation lives in src/mape_k/ (8 files, approximately 1,990 lines).

Architecture

On each tick, the simulator executes the four MAPE phases in order, with the knowledge base recording every adaptation decision:

+----------+   +----------+   +----------+   +----------+
| Monitor  | > | Analyze  | > |   Plan   | > | Execute  |
| (sample  |   | (LTL     |   | (select  |   | (apply   |
|  sensors)|   |  check)  |   |  action) |   |  action) |
+----------+   +----------+   +----------+   +----------+
      ^                                            |
      +------------ Knowledge Base <---------------+

Given system state at tick t, the state transition is:

state(t+1) = Execute(Plan(Analyze(Monitor(state(t), sensors), K(t)), K(t)), K(t))

where Monitor samples sensor values into rolling windows, Analyze evaluates bounded LTL properties over those windows, Plan selects the highest-priority applicable action, and Execute applies the chosen adaptation to the signal state.

The five components

Monitor (src/mape_k/monitor.rs)

The Monitor samples all registered sensor channels each tick and stores values in fixed-capacity ring buffers -- one per signal. The ring buffer overwrites the oldest value when full, maintaining a sliding window of recent history.

Key types:

• Monitor -- holds per-signal rolling windows and the tick counter.
• RingBuffer -- fixed-capacity ring buffer of u64 values.

The window size is configurable but clamped to MAX_WINDOW_SIZE (1,024). A maximum of MAX_SENSORS (64) channels can be tracked.

Analyzer (src/mape_k/analyzer.rs)

The Analyzer evaluates a set of bounded temporal properties against the Monitor's rolling windows each tick. It returns a PropertyResult for each registered property indicating whether it is satisfied or violated, along with the evidence tick.

Key types:

• Analyzer -- holds the property set and evaluates them.
• PropertyResult -- satisfied/violated status with evidence tick offset.

Maximum properties: MAX_PROPERTIES (256).

Planner (src/mape_k/planner.rs)

The Planner holds a fixed-size action table and selects the highest-priority matching action for the current set of property results. Actions are never synthesized on the fly -- they come from a pre-verified library.

Each action entry specifies:

• Which property index triggers it
• Whether it fires on violation or on satisfaction
• A priority (0-255; higher wins ties)

Key types:

• Planner -- holds the action table, performs selection.
• ActionEntry -- maps a property result to an action.
• PlanResult -- the selected action (if any) with context.

Maximum entries: MAX_ACTION_ENTRIES (256).

Executor (src/mape_k/executor.rs)

The Executor applies the planner-selected action to the signal environment. It validates action targets against the declared signal set and captures before/after state snapshots for the knowledge base.

Three action types:

Key types:

• Executor -- applies actions, tracks emergency state.
• ExecutionRecord -- before/after snapshots and success status.

Knowledge Base (src/mape_k/knowledge.rs)

The Knowledge Base maintains a bounded FIFO ring buffer of adaptation records for audit logging. Each record stores the tick, triggering property index, action taken, pre/post state snapshots, and success flag.

When the buffer reaches capacity, the oldest entry is evicted. A monotonic counter tracks lifetime insertions (including evicted records) for completeness audits.

Key types:

• KnowledgeBase -- bounded audit log.
• AdaptationRecord -- one decision record with full context.

Maximum entries: MAX_LOG_ENTRIES (4,096). The knowledge base exports to JSON for DO-254 evidence trails.

Bounded LTL properties

The Analyzer evaluates three bounded temporal operators over rolling signal windows. All algorithms are iterative with O(window_size) complexity per property per tick.

Always -- G(P)

P must hold at every tick in the current window. The analyzer scans the entire window and returns a violation on the first tick where P is false.

TemporalProperty::Always(SignalPredicate::GreaterThan("pressure".into(), 50))

This checks: "pressure must be greater than 50 at every tick in the window."

EventuallyWithin -- F<=N(P)

P must become true at least once within the last N ticks. The analyzer inspects the last N entries and returns satisfied on the first tick where P is true.

TemporalProperty::EventuallyWithin(
    SignalPredicate::IsTrue("alarm_ack".into()),
    100,
)

This checks: "the alarm acknowledgment signal must become nonzero at least once within the last 100 ticks."

Persists -- P for N

P must hold for at least N consecutive ticks anywhere in the window. The analyzer tracks consecutive satisfying ticks and fires when the count reaches N.

TemporalProperty::Persists(
    SignalPredicate::LessThan("pressure".into(), 50),
    10,
)

This checks: "pressure has been below 50 for at least 10 consecutive ticks somewhere in the window." This corresponds directly to the MIRR guard ... for N cycles construct.

Signal predicates

Atomic propositions are evaluated against a single u64 signal value each tick:

Adaptation actions

The planner selects from three action types:

SetSignal

Force a signal to a specific value. The executor validates that the target signal name exists before applying.

AdaptationAction::SetSignal { name: "clamp_valve".into(), value: 1 }

SwitchMode

Switch to a named operating mode. In the R-SPU vision, this selects a pre-synthesized bitstream. In simulation, the mode switch is recorded but signal state is not directly modified.

AdaptationAction::SwitchMode { mode_name: "high_precision".into() }

EmergencyStop

Immediate safety clamp -- zeros all signals to safe defaults. Maps to the R-SPU "Immediate Layer (Static)" reflex. Once triggered, the emergency flag remains active until explicitly cleared.

AdaptationAction::EmergencyStop

Trigger conditions

Each action entry specifies whether it fires on property violation or property satisfaction:

• TriggerCondition::OnViolation -- fire when the property is violated (safety invariant broken). This is the default.
• TriggerCondition::OnSatisfaction -- fire when the property is satisfied (a dangerous condition has been detected and confirmed).

The neonatal monitoring scenario

The MIRR simulator includes a built-in neonatal airway-pressure scenario that exercises the full MAPE-K loop.

Scenario configuration

• Sensor: One channel (airway_pressure), base value 120, noise amplitude 5, fault injection at tick 500 (value drops to 10).
• Properties:
  1. Always(pressure > 50) -- invariant: pressure must never drop below 50.
  2. Persists(pressure < 50, 10) -- sustained anomaly: low pressure for 10 consecutive ticks.
• Actions:
  1. SetSignal("clamp_valve", 1) -- priority 50, fires on invariant violation.
  2. EmergencyStop -- priority 100, fires on sustained low pressure.

Expected behavior

1. Ticks 0-499: Normal operation. Pressure fluctuates around 120 (within noise range 115-125). No violations.
2. Tick 500: Fault injected. Pressure drops to 10. The Always property is immediately violated. The SetSignal action fires (lower priority).
3. Tick 510: The low-pressure condition has persisted for 10 consecutive ticks. The Persists property fires. EmergencyStop (higher priority) is selected, zeroing all signals.
4. Simulation halts after emergency stop.

Sensor model

Each sensor channel uses a deterministic Linear Congruential Generator (LCG) PRNG. Identical seeds produce identical output across runs, ensuring full reproducibility. Fault injection is configured by specifying a start tick, fault value, and optional end tick.

SensorConfig {
    name: "airway_pressure".into(),
    base_value: 120,
    noise_amplitude: 5,
    fault_at_tick: Some(500),
    fault_value: 10,
    fault_end_tick: None,
    seed: 42,
}

API entry points

Running a simulation

use mirr::mape_k::*;

let config = SimConfig {
    sensors: vec![
        SensorConfig {
            name: "airway_pressure".into(),
            base_value: 120,
            noise_amplitude: 5,
            fault_at_tick: Some(500),
            fault_value: 10,
            fault_end_tick: None,
            seed: 42,
        },
    ],
    properties: vec![
        TemporalProperty::Always(
            SignalPredicate::GreaterThan("airway_pressure".into(), 50),
        ),
        TemporalProperty::Persists(
            SignalPredicate::LessThan("airway_pressure".into(), 50),
            10,
        ),
    ],
    action_table: vec![
        ActionEntry {
            trigger_property_idx: 0,
            action: AdaptationAction::SetSignal {
                name: "clamp_valve".into(),
                value: 1,
            },
            priority: 50,
            trigger_on: TriggerCondition::OnViolation,
        },
        ActionEntry {
            trigger_property_idx: 1,
            action: AdaptationAction::EmergencyStop,
            priority: 100,
            trigger_on: TriggerCondition::OnSatisfaction,
        },
    ],
    window_size: 64,
    knowledge_capacity: 1024,
};

let mut sim = MapeKSimulator::new(config);
let result = sim.run(10_000);
println!("{}", result.summary());

Reading the result

The SimResult struct contains:

Exporting the audit trail

let json = sim.knowledge.to_json()?;
std::fs::write("audit_trail.json", json)?;

Bounded iteration guarantees

Every loop and buffer in src/mape_k/ is bounded by a named constant, per NASA Power-of-10 compliance:

The tick count passed to run() is clamped to MAX_TICKS. Window sizes are clamped to MAX_WINDOW_SIZE. Excess properties and action entries beyond their limits are silently truncated.

No unbounded iteration exists in the simulator. The main loop runs for at most MAX_TICKS iterations. Each inner phase (monitor, analyze, plan, execute) iterates over at most MAX_SENSORS, MAX_PROPERTIES, or MAX_ACTION_ENTRIES items respectively.

Knowledge base and audit trail

Every adaptation decision is recorded as an AdaptationRecord:

The knowledge base serializes to JSON for integration with DO-254 evidence trails and other certification workflows.

See Also

• Tutorial -- Getting started with MIRR
• R-SPU Reference -- Instruction set architecture
• Contributing -- Coding standards and campaign workflow