Journal
INFORMATION PROCESSING LETTERS
Volume 135, Issue -, Pages 47-52Publisher
ELSEVIER SCIENCE BV
DOI: 10.1016/j.ipl.2018.02.017
Keywords
Formal semantics; Hybrid systems; Process algebra; Unifying theories; Theorem proving
Categories
Funding
- EU H2020 project INTO-CPS [644047]
- Engineering and Physical Sciences Research Council [EP/G061947/1, EP/E025366/1, EP/H017461/1, EP/D506735/1, EP/M025756/1] Funding Source: researchfish
- EPSRC [EP/M025756/1, EP/H017461/1, EP/R025479/1] Funding Source: UKRI
Ask authors/readers for more resources
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 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. (C) 2018 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available