Back to overview →
Module 01 / 04
Four runtime questions.
Stage 2 starts only after the software model is verified against the mathematical specification.
What the controller must compute.Open section
Mathematical contract
Four runtime questions.
01 / STATE
What changed?
Estimate the extended state Z(t): plant state, physical resources, model validity and active configuration.
02 / CAPABILITY
What can still be done?
Map the remaining resources to functions and mission value for each verified configuration.
03 / ADMISSIBILITY
Which transitions are allowed?
Reject candidates that violate feasibility, stability, safety or the verified configuration graph.
04 / TIMING
When may the switch occur?
Respect reaction latency, switching time and the dwell-time bound before executing a trajectory step.
Evidence from the practical simulation paper
Reported reference implementation results.
Control-loop WCET\(42\,\mu\mathrm{s}\)
Indicator computation\(8\,\mu\mathrm{s}\)
Emergency response\(4.2\,\mathrm{ms}\)
Code + data\(48\,\mathrm{KB}\)
These values are reported for the paper's reference implementation. They are evidence for feasibility, not platform-independent guarantees.