Formal FocusST Specification of CAN
Maria Spichkova
TL;DR
This paper provides a formal specification of the CAN protocol using FocusST, enabling rigorous analysis and verification of its core components with theorem proving tools.
Contribution
It introduces a formal FocusST specification of CAN, facilitating formal analysis and verification of the protocol's core components.
Findings
Formal specification of CAN in FocusST
Foundation for further formal analysis with Isabelle/HOL
Enables rigorous verification of protocol properties
Abstract
This paper presents a formal specification of the Controller Area Network (CAN) protocol using FocusST framework. We formally describe core components of the protocol, which provides a basis for further formal analysis using the Isabelle/HOL theorem prover.
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
TopicsReal-Time Systems Scheduling · Formal Methods in Verification · Petri Nets in System Modeling