TL;DR
This paper extends a pattern-based system for formal property specifications in finite-state verification by incorporating events, which represent variable value changes within LTL, enhancing usability and expressiveness.
Contribution
The paper introduces an extension to existing property patterns by integrating events, allowing for more natural modeling of variable changes in LTL specifications.
Findings
Enhanced pattern system with event representation
Improved readability for non-experts
Facilitated conversion between formal specification languages
Abstract
A pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification was proposed by Dwyer and his collegues. The patterns enable non-experts to read and write formal specifications for realistic systems and facilitate easy conversion of specifications between formalisms, such as LTL, CTL, QRE. In this paper, we extend the pattern system with events - changes of values of variables in the context of LTL.
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.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Logic, programming, and type systems