Skip to content

EFSM Data Path Interval Analysis & Contract Verification

Extended Finite State Machines (EFSM) couple discrete state transitions with continuous or numeric variables. In complex systems, state transitions depend on data path variables (e.g. in.altitude > 1000.0, in.batterySoC < 20.0, reg.retryCount >= 3).

fsmc includes the EFSMIntervalAnalyzer, a static abstract interpretation engine based on interval lattices \([\text{lo}, \text{hi}]\) that propagates variable and port domains forward across all reachable state paths to detect: 1. Unsatisfiable transition guards (dead branches). 2. Out-of-range action assignments violating InPorts, OutPorts, or Registers contracts.

1. Abstract Interpretation Engine

Interval Lattice Mechanics

Each variable in InPorts, OutPorts, and Registers is assigned a domain interval \([\text{lo}, \text{hi}]\) over the extended real numbers \(\mathbb{R} \cup \{-\infty, +\infty\}\):

flowchart TD
    subgraph Propagation["Forward Interval Lattice Propagation"]
        In["InPort Contract: 0.0 to 100.0"] --> Guard{"Guard: x > 50.0"}
        Guard -->|"Intersection: (50.0, 100.0]"| Action["Action: y = x * 2"]
        Action --> Out["OutPort Interval: 100.0 to 200.0"]
    end

    subgraph Join["Convex Hull Join across Merging Paths"]
        PathA["Path A: 10.0 to 20.0"] --> Merge["Convex Hull Join"]
        PathB["Path B: 30.0 to 40.0"] --> Merge
        Merge --> Result["Joined State Domain: 10.0 to 40.0"]
    end
  • InPorts Contracts: Initialized directly from port range annotations (min_value, max_value, e.g. sensor_temp : [-50.0, 150.0]).
  • Registers: Initialized from their default initial value (e.g. cycle_count = 0 \(\implies [0, 0]\)).
  • Assignments mutate intervals:
  • Addition / Subtraction: \([a, b] \pm [c, d] \implies [a \pm c, b \pm d]\)
  • Multiplication: \([a, b] \times [c, d] \implies [\min(ac, ad, bc, bd), \max(ac, ad, bc, bd)]\)
  • Division: \([a, b] / [c, d]\) (safely bounding finite ranges when \(0 \notin [c, d]\))
  • Compound assignment operators (+=, -=, *=, /=) are supported natively across integer and floating-point registers.
  • Variable reset / assignment: v = in.sensor_temp \(\implies \text{Domain}(in.sensor_temp)\)
  • Guard domain constraints:
  • Conjunctions (x >= 10 && x <= 50) intersect interval domains: \([10, +\infty) \cap (-\infty, 50] = [10, 50]\).
  • Disjunctions (x < 5 || x > 20) compute the convex hull join across branches.
  • Negations (!(x < 10)) invert the relational operator (\(x \ge 10\)) to preserve three-valued soundness.
  • State joins compute the least upper bound (convex hull) across converging transition paths:
  • \([10, 20] \sqcup [30, 40] = [10, 40]\)

Formal Widening Operator (\(\nabla\)) for Cyclic Loops

In state machines containing cyclic transitions that mutate variables (e.g. reg.count++, accumulator feedback loops), naive fixed-point iteration may take an unbounded number of steps or fail to terminate.

fsmc implements Cousot & Cousot's formal Widening operator (\(\nabla\)):

\[[a_1, b_1] \mathbin{\nabla} [a_2, b_2] = \left[ \begin{cases} a_1 & \text{if } a_1 \le a_2 \\ -\infty & \text{if } a_2 < a_1 \end{cases}, \quad \begin{cases} b_1 & \text{if } b_2 \le b_1 \\ +\infty & \text{if } b_2 > b_1 \end{cases} \right]\]
  • Guaranteed Termination: When interval bounds strictly increase or decrease across loop iterations, the widening operator immediately projects the diverging bound to \(\pm \infty\).
  • Precision Recovery: After computing the post-fixed-point via widening, a subsequent bounded narrowing iteration sharpens the intervals against explicit guard constraints and port assertions.

2. Dead Branch & Unsatisfiable Guard Detection (W0302)

When evaluating a guarded transition, the analyzer intersects the variable's reachable interval domain with the guard constraint:

\[\text{Domain}(\text{batteryLevel}) \cap (120.0, +\infty) = [0.0, 100.0] \cap (120.0, +\infty) = \emptyset\]

Because the intersection is empty, the guard can never evaluate to true at runtime.

Example: Unsatisfiable Guard

package DroneSystem {
    state def PowerController {
        in port battery_soc : Real { assert constraint { self >= 0.0 and self <= 100.0; } }

        state Cruising;
        state TurboMode;

        // Flaw: battery_soc contract is [0.0, 100.0], so (> 120.0) is mathematically dead
        transition boost first Cruising if in.battery_soc > 120.0 then TurboMode;
    }
}

warning[W0302]: Guard 'in.battery_soc > 120.0' on transition 'Cruising -> TurboMode' is unsatisfiable.
  --> power_controller.sysml:9:9
   |
 9 |         transition boost first Cruising if in.battery_soc > 120.0 then TurboMode;
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Variable range [0.0, 100.0] never satisfies (> 120.0)

```sysml package DroneSystem { state def PowerController { in port battery_soc : Real { assert constraint { self >= 0.0 and self <= 100.0; } }

    state Cruising;
    state TurboMode;

    // Fixed: valid threshold within [0.0, 100.0] domain
    transition boost first Cruising if in.battery_soc > 80.0 then TurboMode;
}

}

[!TIP] Automated Dead Transition Pruning: In optimization modes (-O2 or --prune), transitions identified as having empty guard intersections (\(\text{Domain} \cap \text{Guard} = \emptyset\), classified strictly as EFSMFindingKind::UnsatisfiableGuard) are automatically pruned from the emitted state machine table by DeadStatePruningPass and EFSMDataPathPass, eliminating dead branches completely. Note that out-of-range port or variable contract warnings are reported as diagnostics and do not trigger transition deletion.

3. OutPort Contract Violation Detection

When a transition action assigns an expression whose computed interval falls outside the declared OutPort contract, fsmc flags the out-of-bounds assignment statically.

Example: Contract Range Violation

package ThermalManagement {
    state def HeaterUnit {
        out port heater_duty_cycle : Real { assert constraint { self >= 0.0 and self <= 100.0; } }

        state Standby;
        state Active;

        // Flaw: 150.0 exceeds the declared OutPort contract [0.0, 100.0]
        transition heat first Standby do action { out.heater_duty_cycle = 150.0; } then Active;
    }
}

warning[W_PORT_RANGE_VIOLATION]: OutPort contract violation on transition 'Standby -> Active'.
  --> heater_unit.sysml:9:9
   |
 9 |         transition heat first Standby do action { out.heater_duty_cycle = 150.0; } then Active;
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Value 150.0 exceeds OutPort bound [0.0, 100.0]

package ThermalManagement {
    state def HeaterUnit {
        out port heater_duty_cycle : Real { assert constraint { self >= 0.0 and self <= 100.0; } }

        state Standby;
        state Active;

        // Fixed: clamped value conforming to port contract
        transition heat first Standby do action { out.heater_duty_cycle = 100.0; } then Active;
    }
}

4. Guard Mutual-Exclusivity Analysis (W0301)

When multiple transitions share the same (source_state, trigger_event) and have the same priority, fsmc verifies whether their guard intervals overlap. If an overlap is detected, the transition order is non-deterministic.

Example: Overlapping Guard Collision

package FlightSystem {
    state def NavigationMode {
        in port altitude : Real;

        state Normal;
        state HighAltitude;
        state LowAltitude;

        // Flaw: when altitude is between 500.0 and 800.0, both transitions evaluate to true
        transition to_high first Normal if in.altitude > 500.0 then HighAltitude;
        transition to_low  first Normal if in.altitude < 800.0 then LowAltitude;
    }
}

warning[W0301]: Potentially non-deterministic overlapping guards on state 'Normal'.
  --> navigation.sysml:10:9
   |
10 |         transition to_high first Normal if in.altitude > 500.0 then HighAltitude;
11 |         transition to_low  first Normal if in.altitude < 800.0 then LowAltitude;
   |         -------------------------------------------------------------------------
   |         Intersecting interval (500.0, 800.0) matches multiple unprioritized branches.

package FlightSystem {
    state def NavigationMode {
        in port altitude : Real;

        state Normal;
        state HighAltitude;
        state LowAltitude;

        // Resolution A: Provably disjoint interval bounds
        transition to_high first Normal if in.altitude >= 600.0 then HighAltitude;
        transition to_low  first Normal if in.altitude <  600.0 then LowAltitude;
    }
}

package FlightSystem {
    state def NavigationMode {
        in port altitude : Real;

        state Normal;
        state HighAltitude;
        state LowAltitude;

        // Resolution B: Priority disambiguation (Priority 1 evaluates before Priority 2)
        @fsm:priority 1
        transition to_high first Normal if in.altitude > 500.0 then HighAltitude;

        @fsm:priority 2
        transition to_low  first Normal if in.altitude < 800.0 then LowAltitude;
    }
}

5. Formal SMT & Model Checking Export

The computed interval bounds are automatically fed into the formal backend serializers:

  • nuXmv / NuSMV: Bounded variables (VAR sensor_temp : -50..150;) and contract invariants (INVAR sensor_temp >= -50 & sensor_temp <= 150;).
  • SysML v2: Exported assert constraint { self >= min and self <= max; }.
# Run the full formal verification pipeline via CLI
fsmc -i model.sysml --verify