Unifying Theories of Time with Generalised Reactive Processes
arXiv:1712.10213 · doi:10.1016/j.ipl.2018.02.017
Abstract
Hoare and He's theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.
7 pages, accepted for Information Processing Letters, 15th February 2018
Cited by in corpus (5)
- Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
- Unifying Theories of Reactive Design Contracts
- Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
- Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
- Automated Verification of Reactive and Concurrent Programs by Calculation