Bounded Model Checking of Temporal Formulas with Alloy
Alcino Cunha (HASlab / INESC TEC, Universidade do Minho)
TL;DR
This paper introduces a method to perform bounded model checking of reactive systems specified with temporal logic using the Alloy Analyzer, extending Alloy's capabilities for system verification.
Contribution
It proposes integrating temporal logic into Alloy and demonstrates how to perform bounded model checking within this framework, addressing Alloy's lack of native support for reactive systems.
Findings
Temporal logic can be effectively used to specify reactive systems in Alloy.
Bounded model checking of temporal formulas is feasible with the Alloy Analyzer.
The approach extends Alloy's applicability to reactive system verification.
Abstract
Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be performed with the Alloy Analyzer.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.