CS6315-Project

This project implements automated verification of probabilistic sensor systems using StormPy and PRISM. The main focus is modeling a kitchen environment with sensors and actuators (burners, smoke detectors, temperature sensors), where each component may fail or behave probabilistically. The goal is to formally verify safety properties and analyze system behavior under uncertainty.

Small video talking about this project:

Project Overview

The system is modeled as a Discrete-Time Markov Chain (DTMC):

Each state represents a specific configuration of the kitchen environment:

• Burner status (on/off)
• Temperature levels
• Smoke detection status

Transitions capture probabilistic events:

• Sensor failures
• Random fluctuations in temperature or smoke detection

Safety properties are specified using Probabilistic Computation Tree Logic (PCTL).

Example properties:

• Probability of reaching a fire risk state
• Likelihood that cooling prevents overheating
• Threshold checks for hazards (gas exposure)

The project also demonstrates simulation-based analysis (Monte Carlo) for exploring how probabilistic failures impact overall system behavior. This was used to understand the capablilities of the PCTL model checking structure and serve as a comparison to formal verification results.

Requirements

This project is designed to run in WSL or Docker due to StormPy’s reliance on Storm (not fully supported on Windows).

Python Dependencies

Install the required Python packages:

pip install -r requirements.txt

Graphviz

sudo apt update
sudo apt install graphviz

Setup and Usage

Create and activate a Python virtual environment:

source venv/Scripts/Activate

From the src directory run,

 python main.py

or to run the monte_carlo simulation.

 python main.py --experimental

Transition Models:

The main goal I had when creating these models was selecting a small handful real world systems that would be found in a kitchen that use or could use sensors. Due to this I decided to create 4 models that would be found within this environment. The models are:

Gas Sensor Model: Checks for gas leaks and exposure thresholds.

Kitchen Stove Model: Monitors burner status, temperature, and smoke.

Water Sensor Model: Monitors potential water quality and sensor alerts.

Refrigerator Model: Monitors device health (doors open) and possibly temperature irregularities

Each model includes:

• DTMC representation in PRISM

• PCTL safety and reachability properties

• Optional Monte Carlo simulation for selected variables

Probabilistic Transition System

In this project, the transition system is:

Probabilistic: Transitions between states occur with defined probabilities.

State-based: Each state encodes all relevant system variables.

Analyzable: Using PCTL and model checking, we can compute:

• Probability of reaching unsafe states

• Expected number of steps to hazards

• Per-state property values

• Simulatable: Monte Carlo simulations allow exploration of probabilistic behaviors across multiple runs.

Results and Takeaways:

PCTL Logic Checks

I have applied several PCTL logic checks, divided into the following categories:

• Reachability: Verifying whether certain states can eventually be reached.
• Time-Bounded: Checking if states are reached within a specified number of steps.
• Threshold / Safety Checks: Ensuring that probabilities of unsafe states remain below defined thresholds.
• Expected Steps (Rewards): Estimating the expected number of steps to reach certain states.

The Monte Carlo simulation complements these analyses by reflecting the expected steps and rewards, providing an empirical perspective on system behavior under probabilistic failures.

Comparison of PCTL Expected Steps and Monte Carlo Simulation

A few examples explored using the monte carlo simulation include:

• Gas Sensor Model: gas_hazard

• Refrigerator Model: at_risk

• Stove Model: fire_risk

• Water Sensor Model: water_leak

For the Gas Sensor Model property gas_hazard:

PCTL Expected Steps (Reward-Based)

• Per-state expected steps to reach gas_hazard:
  {52.8571, 2.85714, 1.42857, 0, 0}

These values indicate how many steps it is expected to take for the system to reach the gas_hazard state when starting from each state.

Monte Carlo Simulation Results

• Mean steps: 50.49
• Median steps: 37
• Min: 3
• Max: 199
• Fraction reached within bounded time: 0.283

This summarizes how long it took in simulation for the system to reach the gas_hazard condition from the initial state.

Interpretation

The PCTL analysis shows that some states reach gas_hazard very quickly (1–3 steps), while others may take significantly longer (53 steps). The Monte Carlo results closely align with this expectation: the mean number of steps (50) is very similar to the PCTL expectation for the initial state.

The median (37) is lower than the mean, indicating that in many runs the hazard occurs faster than expected, but the tail of long runs (up to 199 steps) pulls the average upward. The fraction reached (0.283) suggests moderate likelihood of entering a hazard state within bounded time.

Overall, the formal model and empirical simulation agree, validating both the model and the hazard assumptions.

For the Refrigerator Model property at_risk:

PCTL Expected Steps (Reward-Based)

• Result per state:
  {100.432, 80.4322, 54.7179, 100.096, 0, 0, 0, 0}

This represents the expected number of steps for the system to first reach the at_risk state from each initial state.

Monte Carlo Simulation Results

• Time statistics for at_risk:
• Mean: 70.97
• Median: 57
• Min: 3
• Max: 199
• Fraction of runs reaching the state within the bounded time: 0.152

This starts from the initial state until it reaches the at_risk state.

Interpretation

The PCTL results suggest the system may require many steps (55–100+) before reaching the at_risk state from most initial configurations. The Monte Carlo simulation confirms that reaching this state typically takes dozens of steps (median 57), but may occur much earlier or much later depending on randomness.

The fraction reached (0.152) indicates that only about 15% of simulated runs entered the risky state within the time bound, which matches the expectation that the refrigerator is usually safe unless a rare sequence of events unfolds.

This alignment suggests that the at_risk state is uncommon and generally slow to appear, reinforcing system robustness.

For the Stove Model property fire_risk:

PCTL Expected Steps (Reward-Based)

Result per state:

[
198.75952175312037,
197.75952175312037,
196.6484106420093,
192.08050940744138,
181.048273467798,
200.0095217531204,
156.36910870632863,
201.25952175312034,
102.87976087656016,
202.5095217531203,
0.0,
203.75952175312025,
Infinity,
Infinity,
Infinity,
Infinity,
Infinity,
Infinity
]

These values represent the expected number of steps before the system reaches the fire_risk state from each state in the model.
States with Infinity cannot reach the fire_risk condition.

Monte Carlo Simulation Results

• Mean steps: 83.68
• Median steps: 75
• Min: 7
• Max: 199
• Fraction reached within bounded time: 0.094

The Monte Carlo simulation shows that fire_risk is reached relatively rarely and typically after many steps.

Interpretation

The PCTL results show that many states require a very large expected number of steps (180–200+) before reaching fire_risk, and several states cannot reach fire risk at all (Infinity). This matches the design intention that fire risk is a rare, high-threshold event.

Monte Carlo results reinforce this: the hazard is only reached in a small fraction of runs (0.094), and even then it typically takes a long time (mean 84 steps).

Together, these findings confirm that fire events are both rare and slow to develop, though still possible under unlucky or unsafe conditions.

For the Water Sensor Model property water_leak:

PCTL Expected Steps (Reward-Based)

Result per state:

[
239.99999999999707,
219.9999999999973,
0.0
]

These represent the expected number of steps before the system reaches the water_leak state from each initial state.
State 2 has a value of 0, meaning it already satisfies the water_leak condition.

Monte Carlo Simulation Results

• Mean steps: 89.03
• Median steps: 78
• Min: 2
• Max: 197
• Fraction reached within bounded time: 0.067

This indicates that water leaks occur infrequently and usually after many steps in simulated runs.

Interpretation

The PCTL values show extremely long expected times to reach a water_leak (220–240 steps), and the Monte Carlo results confirm that leaks happen rarely (fraction 0.067) and usually only after many steps.

The discrepancy between PCTL expectations (220–240) and Monte Carlo mean (89) is likely due to the simulation’s time bound and early termination effects — the simulation may not fully explore long-running sequences where leaks eventually occur.

Despite this difference, both methods indicate that water leaks are low-probability, slow-to-develop events.