Quickstart Tutorial¶
This tutorial walks through creating a complete, production-ready aerospace sub-system state machine from scratch, verifying its safety properties, and embedding it in C++ using fsmc.
Scenario: Autonomous UAV Flight Controller¶
We will model a flight mission state machine with three operating modes:
- Preflight: Sensor calibration and motor arming.
- Navigating: Waypoint navigation with emergency low-battery fail-safe return.
- Landed: Final disarm and shutdown.
Step 1: Author the State Machine Model¶
Choose your preferred modeling syntax to define the UAV state machine with typed I/O ports and internal registers:
package UavMissionSystem {
state def UavMissionStatechart {
in port isGpsLocked : Boolean;
in port batteryLevel : Real { assert constraint { self >= 0.0 and self <= 100.0; } }
out port waypointReached : Boolean;
attribute cycleCounter : Integer = 0;
entry; then SensorCalib;
state SensorCalib {
accept CalibrationOk then SystemReady;
}
state SystemReady {
accept TakeoffCmd if in.isGpsLocked then WaypointNav;
}
state WaypointNav {
accept AreaReached do MarkWaypointReached then HoverPause;
accept LowBatteryEvent if in.batteryLevel < 20.0 then ReturnToHome;
}
state HoverPause {
accept ResumeMissionCmd then WaypointNav;
accept LowBatteryEvent if in.batteryLevel < 20.0 then ReturnToHome;
}
state ReturnToHome {
accept TouchdownEvent then Landed;
}
state Landed {
accept ShutdownCmd then FinalShutdown;
}
state FinalShutdown;
}
}
@startuml
[*] --> SensorCalib
SensorCalib --> SystemReady : CalibrationOk
SystemReady --> WaypointNav : TakeoffCmd [in.isGpsLocked]
WaypointNav --> HoverPause : AreaReached / out.waypointReached=true
WaypointNav --> ReturnToHome : LowBatteryEvent [in.batteryLevel < 20.0]
HoverPause --> WaypointNav : ResumeMissionCmd
HoverPause --> ReturnToHome : LowBatteryEvent [in.batteryLevel < 20.0]
ReturnToHome --> Landed : TouchdownEvent
Landed --> [*] : ShutdownCmd
@enduml
Step 2: Formally Verify the State Machine¶
Run fsmc with the --verify option to run middle-end passes (deadlock detection, choice completeness, interval domain analysis):
Expected output:
============================================================================
Formal Model Verification Report: UavMissionStatechart
============================================================================
Input File: uav_mission.sysml
States: 7
Total Events: 7
Transitions: 8
Choice Nodes: 0
Deferred Triggers:0
----------------------------------------------------------------------------
Diagnostics:
(No warnings or errors detected. Model is formally sound!)
----------------------------------------------------------------------------
Verification Status: PASSED (Model Sound & Properties Verified)
============================================================================
Step 3: Generate the State Machine¶
Compile the model into a standalone C++20 header with namespace avionics and class name UavMissionFSM:
[!NOTE] Upcoming Target Preview: Rust code generation is currently in development under the multi-target roadmap. C++ is the active production runtime.
Compile the model into an idiomatic #![no_std] Rust module:
[!NOTE] Upcoming Target Preview: ISO C99 embedded C code generation is currently in development under the multi-target roadmap. C++ is the active production runtime.
Compile the model into deterministic, zero-heap C headers and sources:
Step 4: Write the Application Code¶
Create main.cpp:
#include "uav_mission_fsm.hpp"
#include <cassert>
#include <iostream>
int main() {
using namespace avionics;
// 1. Initialize internal registers and state machine
UavMissionFSMRegisters reg{0};
UavMissionFSM fsm(reg);
// 2. Setup I/O port structures
UavMissionFSMInPorts in;
in.batteryLevel = 98.5;
in.isGpsLocked = true;
UavMissionFSMOutPorts out;
assert(in.validate_contracts());
std::cout << "Current State: " << fsm.current_state_name() << "\n";
// Output: SensorCalib
// 3. Dispatch calibration completion event
fsm.dispatch(CalibrationOk{}, in, out);
std::cout << "Current State: " << fsm.current_state_name() << "\n";
// Output: SystemReady
// 4. Dispatch takeoff command (guard evaluated against in.isGpsLocked)
auto result = fsm.dispatch(TakeoffCmd{}, in, out);
if (result.is_success()) {
std::cout << "Takeoff successful. Current State: " << fsm.current_state_name() << "\n";
// Output: WaypointNav
}
// 5. Simulate battery drop in InPorts and dispatch LowBatteryEvent
in.batteryLevel = 14.2; // Critical level (< 20.0)
auto safe_res = fsm.dispatch(LowBatteryEvent{}, in, out);
if (safe_res.is_success()) {
std::cout << "Emergency fail-safe activated. Transitioned to: "
<< fsm.current_state_name() << "\n";
// Output: ReturnToHome
}
return 0;
}
[!NOTE] Upcoming Target Preview: Preview of planned
#![no_std]Rust application integration.
Create main.rs:
use avionics::uav_mission_fsm::*;
fn main() {
let mut fsm = UavMissionFsm::new(UavRegisters::default());
let mut in_ports = UavInPorts { battery_level: 98.5, is_gps_locked: true };
let mut out_ports = UavOutPorts::default();
println!("Current State: {:?}", fsm.state());
// 1. Dispatch calibration completion event
fsm.dispatch(&Event::CalibrationOk, &in_ports, &mut out_ports);
println!("Current State: {:?}", fsm.state());
// 2. Dispatch takeoff command
let res = fsm.dispatch(&Event::TakeoffCmd, &in_ports, &mut out_ports);
if res.is_transitioned() {
println!("Takeoff successful. Current State: {:?}", fsm.state());
}
// 3. Dispatch LowBatteryEvent (battery drop)
in_ports.battery_level = 14.2;
let safe_res = fsm.dispatch(&Event::LowBatteryEvent, &in_ports, &mut out_ports);
if safe_res.is_transitioned() {
println!("Emergency fail-safe activated. Transitioned to: {:?}", fsm.state());
}
}
[!NOTE] Upcoming Target Preview: Preview of planned ISO C99 embedded C application integration.
Create main.c:
#include "uav_mission_fsm.h"
#include <stdio.h>
#include <assert.h>
int main(void) {
avionics_uav_fsm_t fsm;
avionics_registers_t reg = {0};
avionics_in_ports_t in = {.battery_level = 98.5f, .is_gps_locked = true};
avionics_out_ports_t out = {0};
avionics_uav_fsm_init(&fsm, ®);
printf("Current State: %d\n", fsm.current_state);
/* 1. Dispatch calibration completion */
avionics_uav_fsm_dispatch(&fsm, AVIONICS_EV_CALIB_OK, &in, &out);
printf("Current State: %d\n", fsm.current_state);
/* 2. Dispatch takeoff command */
fsm_result_t res = avionics_uav_fsm_dispatch(&fsm, AVIONICS_EV_TAKEOFF, &in, &out);
if (res == FSM_TRANSITIONED) {
printf("Takeoff successful. Current State: %d\n", fsm.current_state);
}
/* 3. Dispatch LowBatteryEvent (battery drop) */
in.battery_level = 14.2f;
avionics_uav_fsm_dispatch(&fsm, AVIONICS_EV_LOW_BATTERY, &in, &out);
printf("Emergency fail-safe activated. Transitioned to: %d\n", fsm.current_state);
return 0;
}
Step 5: Compile and Run¶
Output: