ExMaude.IoT (ExMaude v0.2.0)

View Source

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

  1. 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.

  2. Environment Conflict - Two rules produce opposing environmental effects. Example: one rule opens a window to cool, another closes it to reduce noise.

  3. State Cascade - A rule's output triggers another rule, creating unexpected chains. Example: door open → light on → play sound → light off creates oscillation.

  4. 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()
thing_id()
trigger()

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.

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()
}

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()}

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.