vIRONy
A tool for verifying Event-Condition-Action rules in Intelligent Environments (smart homes, e-health) — an IRON-language parser and Eclipse-like IDE backed by the T2 and Z3 SMT solvers.
- Z3 SMT
- T2
- IRON DSL
- Formal Verification
My role
Built vIRONy — verification of Event-Condition-Action (ECA) rules for Intelligent Environments: a dedicated parser for the IRON language, an Eclipse-like editor interface, and verification via the T2 termination prover and the Z3 SMT solver, combined with configurable simulation.
Outcome
Published at IEEE Intelligent Environments (2017).
Intelligent Environments (IE) are technological ecosystems that interact with and adapt to their inhabitants — smart homes, autonomous vehicles, and more — operating on rules. As they integrate ever more deeply into daily life, ensuring these rule-based systems are reliable and safe becomes vital. vIRONy addresses the challenges of verifying them.
Challenge
Intelligent Environments span sectors from smart homes to e-healthcare, and the unpredictable nature of rule interactions makes rigorous verification difficult.
Solution
vIRONy assists in verifying Event-Condition-Action (ECA) rules. By combining formal methods with simulation, it supports developers and end-users throughout modeling and verification. Programs first undergo a syntactic-correctness check; successful ones proceed to formal verification and simulation, culminating in a thorough analysis of system behavior and performance.
Technical details
vIRONy incorporates a dedicated parser for the IRON language, an interface reminiscent of the Eclipse IDE, and relies on T2 and the Z3 SMT solver for verification — handling rule systems whose state spaces exceed 20 million states. Simulations are adjustable by user configuration and rooted in a specific model.
Key features
- The GUI handles tasks such as input-file selection and simulation-graph visualization.
- Ensures programmatic correctness.
- Employs formal tools for verification.
- Provides insight into potential system behaviors.
- Offers a comprehensive breakdown of the simulation.
Demo
Want something built like this? I'm available for contract work.