Timed Concurrent State Machines
Wiktor B. Daszczuk
TL;DR
This paper introduces Timed Concurrent State Machines, extending CSMs with timing features based on Timed Automata, enabling easier specification of time properties and efficient verification through a global state space.
Contribution
It presents a novel timed extension of CSMs, called TCSM, and a method for real-time global state space calculation for system verification.
Findings
Supports easier specification of time properties.
Defines real-time global state space calculation.
Enables verification-ready system modeling.
Abstract
Timed Concurrent State Machines are an application of Alur's Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to store a verified system in ready-to-verification form, and to multiply it by various testing automata.
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 · Machine Learning and Algorithms · Software Testing and Debugging Techniques