vIRONy
Intelligent Environments (IE) are technological ecosystems that interact with and adapt to their inhabitants. These systems, prevalent in applications like smart homes and autonomous vehicles, operate based on rules. Ensuring the reliable and safe operation of these rule-based systems is vital, with their increasing integration into daily life. vIRONy addresses the challenges tied to system verification.
Challenge
IE, expanding across sectors like smart homes and e-healthcare, necessitate rigorous verification. The unpredictable nature of rule interactions further complicates this task.
Solution
The introduction of vIRONy assists in the verification of Event-Condition-Action (ECA) rules. By combining formal methods with simulation techniques, this tool aids developers and end-users throughout the modeling and verification processes.
Process
Programs undergo an initial syntactic correctness assessment. Successful checks are followed by formal verifications and simulations, culminating in a thorough analysis of system behaviors and performance.
Technical Details
vIRONy incorporates a dedicated parser for the IRON language, an interface reminiscent of the Eclipse IDE, and relies on tools like T2 and the SMT solver Z3 for verification. The simulations, adjustable by user configurations, are rooted in a specific model.
Key Features
- The GUI facilitates tasks such as input file selection and simulation graph visualization.
- The tool ensures programmatic correctness.
- Employs tools for verification.
- Provides insights into potential system behaviors.
- Offers a comprehensive breakdown of the simulation.
If you want to know more about vIRONy, please check out the [gitlab], [paper], and demo video:
