View Source cure_fsm_monitor (cure v0.7.0)

Cure FSM Runtime Verification

This module implements runtime verification for FSMs by generating monitors from verified properties and injecting runtime assertions.

Features

  • Property Monitors: Generate runtime monitors from safety/liveness properties
  • Assertion Injection: Inject runtime assertions into FSM transitions
  • Violation Detection: Detect and report property violations at runtime
  • Counterexample Generation: Provide traces when properties are violated
  • Performance Overhead: < 5% overhead for monitored FSMs

Monitor Types

  1. Safety Monitors: Ensure bad states are never reached
  2. Liveness Monitors: Ensure progress is always possible
  3. Deadlock Monitors: Detect deadlock conditions
  4. Custom Monitors: User-defined property monitors

Usage 

% Generate monitor from property
Monitor = cure_fsm_monitor:generate_monitor(FsmDef, {safety, [BadState]}),

% Inject monitor into FSM
MonitoredFsm = cure_fsm_monitor:inject_monitor(FsmDef, Monitor),

% Start monitored FSM
{ok, Pid} = cure_fsm_runtime:start_fsm(MonitoredFsm, InitData),

% Monitor will report violations
receive
    {monitor_violation, Pid, Violation} ->
        io:format("Property violated: ~p~n", [Violation])
end.

Summary

Functions

check_assertion(Assertion, Context)
check_property(FsmPid, Property, CurrentState)
disable_monitor(FsmDef, MonitorId)
enable_monitor(FsmDef, MonitorId)
format_violation(Violation)
generate_deadlock_monitor(FsmDef)
generate_liveness_monitor(FsmDef)
generate_monitor(FsmDef, Property)
generate_safety_monitor(FsmDef, BadStates)
inject_monitor(FsmDef, Monitor)
inject_monitors(FsmDef, Monitors)
list_monitors(FsmDef)
report_violation(State, Monitor, Violation)

Functions

check_assertion(Assertion, Context)

-spec check_assertion(Assertion :: term(), Context :: term()) -> ok | {violation, term()}.

check_property(FsmPid, Property, CurrentState)

-spec check_property(FsmPid :: pid(), Property :: term(), CurrentState :: atom()) ->
                        ok | {violation, term()}.

disable_monitor(FsmDef, MonitorId)

-spec disable_monitor(FsmDef :: term(), MonitorId :: atom()) -> term().

enable_monitor(FsmDef, MonitorId)

-spec enable_monitor(FsmDef :: term(), MonitorId :: atom()) -> term().

format_violation(Violation)

-spec format_violation(Violation :: term()) -> binary().

generate_deadlock_monitor(FsmDef)

-spec generate_deadlock_monitor(FsmDef :: term()) ->
                                   #fsm_monitor{id :: atom(),
                                                type :: safety | liveness | deadlock | custom,
                                                property :: term(),
                                                check_fn ::
                                                    fun((term(), term()) -> ok | {violation, term()}),
                                                enabled :: boolean(),
                                                violations :: [term()]}.

generate_liveness_monitor(FsmDef)

-spec generate_liveness_monitor(FsmDef :: term()) ->
                                   #fsm_monitor{id :: atom(),
                                                type :: safety | liveness | deadlock | custom,
                                                property :: term(),
                                                check_fn ::
                                                    fun((term(), term()) -> ok | {violation, term()}),
                                                enabled :: boolean(),
                                                violations :: [term()]}.

generate_monitor(FsmDef, Property)

-spec generate_monitor(FsmDef :: term(), Property :: term()) ->
                          #fsm_monitor{id :: atom(),
                                       type :: safety | liveness | deadlock | custom,
                                       property :: term(),
                                       check_fn :: fun((term(), term()) -> ok | {violation, term()}),
                                       enabled :: boolean(),
                                       violations :: [term()]}.

generate_safety_monitor(FsmDef, BadStates)

-spec generate_safety_monitor(FsmDef :: term(), BadStates :: [atom()]) ->
                                 #fsm_monitor{id :: atom(),
                                              type :: safety | liveness | deadlock | custom,
                                              property :: term(),
                                              check_fn ::
                                                  fun((term(), term()) -> ok | {violation, term()}),
                                              enabled :: boolean(),
                                              violations :: [term()]}.

inject_monitor(FsmDef, Monitor)

-spec inject_monitor(FsmDef :: term(),
                     Monitor ::
                         #fsm_monitor{id :: atom(),
                                      type :: safety | liveness | deadlock | custom,
                                      property :: term(),
                                      check_fn :: fun((term(), term()) -> ok | {violation, term()}),
                                      enabled :: boolean(),
                                      violations :: [term()]}) ->
                        term().

inject_monitors(FsmDef, Monitors)

-spec inject_monitors(FsmDef :: term(),
                      Monitors ::
                          [#fsm_monitor{id :: atom(),
                                        type :: safety | liveness | deadlock | custom,
                                        property :: term(),
                                        check_fn :: fun((term(), term()) -> ok | {violation, term()}),
                                        enabled :: boolean(),
                                        violations :: [term()]}]) ->
                         term().

list_monitors(FsmDef)

-spec list_monitors(FsmDef :: term()) -> [atom()].

report_violation(State, Monitor, Violation)

-spec report_violation(State :: term(),
                       Monitor ::
                           #fsm_monitor{id :: atom(),
                                        type :: safety | liveness | deadlock | custom,
                                        property :: term(),
                                        check_fn :: fun((term(), term()) -> ok | {violation, term()}),
                                        enabled :: boolean(),
                                        violations :: [term()]},
                       Violation :: term()) ->
                          ok.