ExMaude.IoT (ExMaude v0.3.0)

IoT rule conflict detection using Maude formal verification.

This module provides an Elixir API for detecting conflicts in IoT automation rules using Maude's formal verification capabilities. It implements the four conflict types identified in the AutoIoT paper (arxiv.org/abs/2411.10665):

Conflict Types

State Conflict - Two rules target the same device property with incompatible values. Example: motion sensor turns light on while time-based rule turns it off.
Environment Conflict - Two rules produce opposing environmental effects. Example: one rule opens a window to cool, another closes it to reduce noise.
State Cascade - A rule's output triggers another rule, creating unexpected chains. Example: door open → light on → play sound → light off creates oscillation.
State-Environment Cascade - Combined state and environment effects cascade through multiple rules. Example: AC on → window closes → CO2 rises → window opens → conflicts with AC.

Usage

# Define rules
rules = [
  %{
    id: "motion-light",
    thing_id: "light-1",
    trigger: {:prop_eq, "motion", true},
    actions: [{:set_prop, "light-1", "state", "on"}],
    priority: 1
  },
  %{
    id: "night-light",
    thing_id: "light-1",
    trigger: {:prop_gt, "time", 2300},
    actions: [{:set_prop, "light-1", "state", "off"}],
    priority: 1
  }
]

# Detect conflicts (the bundled iot-rules.maude module is loaded
# automatically on first call)
{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)
# => [%{type: :state_conflict, rule1: "motion-light", rule2: "night-light", ...}]

Telemetry

This module emits the following telemetry events:

[:ex_maude, :iot, :detect_conflicts, :start] - Emitted when detection begins
[:ex_maude, :iot, :detect_conflicts, :stop] - Emitted when detection completes

Measurements include :duration in native time units, :rule_count, and :conflict_count. Metadata includes :result (:ok or :error) and :template (:iot_rules).

See ExMaude.Telemetry for full event documentation and integration examples.

Summary

Types

action()

conflict()

conflict_type()

rule()

state_pred()

A predicate over a world state: a device property holding a value, or an environment key holding a value.

thing_id()

trigger()

world_opts()

Options for the state-space verification functions.

Functions

detect_cascade_conflicts(rules, opts \\ [])

Detects cascade conflicts (both state and state-environment).

detect_conflicts(rules, opts \\ [])

Detects all conflicts in a set of IoT rules.

detect_env_conflicts(rules, opts \\ [])

Detects only environment conflicts in a set of rules.

detect_state_conflicts(rules, opts \\ [])

Detects only state conflicts in a set of rules.

validate_rule(rule)

Validates a rule structure without sending it to Maude.

validate_rules(rules)

Validates a list of rules.

verify_liveness(rules, goal_state, opts \\ [])

Bounded liveness check: looks for a deadlock that prevents rules from reaching goal_state.

verify_safety(rules, bad_state, opts \\ [])

Bounded safety check: proves no execution of rules reaches a world matching bad_state.

Types

action()

@type action() ::
  {:set_prop, thing_id(), String.t(), term()}
  | {:set_env, String.t(), term()}
  | {:invoke, thing_id(), String.t()}

conflict()

@type conflict() :: %{
  type: conflict_type(),
  rule1: String.t(),
  rule2: String.t(),
  reason: String.t()
}

conflict_type()

@type conflict_type() ::
  :state_conflict | :env_conflict | :state_cascade | :state_env_cascade

rule()

@type rule() :: %{
  :id => String.t(),
  :thing_id => thing_id(),
  :trigger => trigger(),
  :actions => [action()],
  optional(:priority) => non_neg_integer()
}

state_pred()

@type state_pred() ::
  {:thing_state, thing_id(), String.t(), term()}
  | {:env_state, String.t(), term()}

A predicate over a world state: a device property holding a value, or an environment key holding a value.

thing_id()

@type thing_id() :: String.t()

trigger()

@type trigger() ::
  {:prop_eq, String.t(), term()}
  | {:prop_gt, String.t(), number()}
  | {:prop_lt, String.t(), number()}
  | {:prop_gte, String.t(), number()}
  | {:prop_lte, String.t(), number()}
  | {:env_eq, String.t(), term()}
  | {:env_gt, String.t(), number()}
  | {:env_lt, String.t(), number()}
  | {:always}
  | {:and, trigger(), trigger()}
  | {:or, trigger(), trigger()}
  | {:not, trigger()}

world_opts()

@type world_opts() :: [
  initial_state: [state_pred()],
  max_depth: pos_integer(),
  timeout: timeout()
]

Options for the state-space verification functions.

:initial_state - bindings present before any rule fires (default [])
:max_depth - bound on search depth (default 50); unbounded searches that hit the bound return {:ok, :unverified} rather than blocking
:timeout - per-search timeout in ms (default 30_000)

Functions

detect_cascade_conflicts(rules, opts \\ [])

@spec detect_cascade_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects cascade conflicts (both state and state-environment).

Cascade conflicts occur when one rule's output triggers another rule.

detect_conflicts(rules, opts \\ [])

@spec detect_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects all conflicts in a set of IoT rules.

Analyzes the given rules for all four conflict types using Maude formal verification. Returns a list of detected conflicts, or an empty list if no conflicts are found.

Examples

rules = [
  %{id: "r1", thing_id: "light-1", trigger: {:prop_eq, "motion", true},
    actions: [{:set_prop, "light-1", "state", "on"}], priority: 1},
  %{id: "r2", thing_id: "light-1", trigger: {:prop_gt, "time", 2300},
    actions: [{:set_prop, "light-1", "state", "off"}], priority: 1}
]

{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)
[%{type: :state_conflict, rule1: "r1", rule2: "r2", reason: _}] = conflicts

Options

:timeout - Maximum time in milliseconds (default: 10000)
:conflict_types - List of conflict types to check (default: all)

detect_env_conflicts(rules, opts \\ [])

@spec detect_env_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects only environment conflicts in a set of rules.

Environment conflicts occur when two rules produce opposing environmental effects.

detect_state_conflicts(rules, opts \\ [])

@spec detect_state_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects only state conflicts in a set of rules.

State conflicts occur when two rules target the same device property with incompatible values.

Examples

{:ok, conflicts} = ExMaude.IoT.detect_state_conflicts(rules)

validate_rule(rule)

@spec validate_rule(rule()) :: :ok | {:error, [String.t()]}

Validates a rule structure without sending it to Maude.

Returns :ok if the rule is valid, or {:error, errors} with a list of validation error messages.

Examples

:ok = ExMaude.IoT.validate_rule(%{
  id: "my-rule",
  thing_id: "device-1",
  trigger: {:prop_eq, "state", true},
  actions: [{:set_prop, "device-1", "power", "on"}]
})

{:error, ["missing required field: id"]} = ExMaude.IoT.validate_rule(%{})

validate_rules(rules)

@spec validate_rules([rule()]) ::
  :ok | {:error, %{required(String.t()) => [String.t()]}}

Validates a list of rules.

Returns :ok if all rules are valid, or {:error, errors} with a map of rule IDs to their validation errors.

verify_liveness(rules, goal_state, opts \\ [])

@spec verify_liveness([rule()], state_pred(), world_opts()) ::
  {:ok, :live}
  | {:ok, :unverified}
  | {:error, :deadlock_possible | ExMaude.Error.t() | term()}

Bounded liveness check: looks for a deadlock that prevents rules from reaching goal_state.

Searches for a terminal world (=>!, no rule can fire) in which goal_state does not hold. Because the search only inspects terminal states, this detects deadlocks (the system stops short of the goal); it does not detect livelocks (infinite progress that never reaches the goal), which need full LTL model checking.

Returns:

{:ok, :live} - every reachable terminal world satisfies goal_state
{:error, :deadlock_possible} - a reachable terminal world misses the goal
{:ok, :unverified} - Maude unavailable or timed out — undecided
{:error, %ExMaude.Error{}} - the verification itself failed (invalid rule encoding, missing module, ...)

Examples

ExMaude.IoT.verify_liveness(rules, {:thing_state, "door", "state", "notified"})
#=> {:ok, :live}

verify_safety(rules, bad_state, opts \\ [])

@spec verify_safety([rule()], state_pred() | [state_pred()], world_opts()) ::
  {:ok, :safe}
  | {:ok, :unverified}
  | {:error, {:counterexample, [map()]} | ExMaude.Error.t() | term()}

Bounded safety check: proves no execution of rules reaches a world matching bad_state.

Explores the rule-firing transition system (the IOT-EXEC Maude module) from the initial state with =>* reachability search, looking for a reachable world whose state contains bad_state.

Returns:

{:ok, :safe} - no bad world reachable within max_depth
{:error, {:counterexample, solutions}} - a reachable bad world (the solutions carry the matching state/substitution)
{:ok, :unverified} - Maude unavailable or timed out — unable to decide (absence of proof, not evidence of safety)
{:error, %ExMaude.Error{}} - the verification itself failed (e.g. a rule that doesn't encode to valid Maude, or a missing module); surfaced as an error rather than :unverified because it indicates a bug in the input, not an inconclusive search

bad_state is a state_pred or a list of them (a list means "all present in the same reachable world").

Examples

# Rule drives a door into an error state when motion is detected.
rules = [%{id: "r1", thing_id: "door", trigger: {:prop_eq, "motion", true},
           actions: [{:set_prop, "door", "state", "error"}], priority: 1}]

ExMaude.IoT.verify_safety(rules, {:thing_state, "door", "state", "error"},
  initial_state: [{:thing_state, "door", "motion", true}])
#=> {:error, {:counterexample, [_ | _]}}