Statechart Verification with iState
Dai Tri Man Le
TL;DR
This paper presents an algorithm for verifying statecharts using the iState tool, introducing a novel predicate semantics approach that enhances formal analysis of statechart models.
Contribution
It introduces a detailed verification algorithm for statecharts and a new predicate semantics framework, advancing formal verification methods for state-based models.
Findings
Verification conditions can be systematically generated from statecharts.
The predicate semantics approach provides a new way to interpret statecharts formally.
The iState tool effectively implements the proposed verification algorithm.
Abstract
This paper is the longer version of the extended abstract with the same name published in FM 06. We describe in detail the algorithm to generate verification conditions from statechart structures implemented in the iState tool. This approach also suggests us a novel method to define a version of predicate semantics for statecharts analogous to how we assign predicate semantics to programming languages.
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 · Petri Nets in System Modeling · Model-Driven Software Engineering Techniques