zbMATH — the first resource for mathematics

Unifying theories of time with generalised reactive processes. (English) Zbl 06856068
Summary: 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.

68Q Theory of computing
Circus; Isabelle/HOL
Full Text: DOI
[1] Hoare, C. A.R.; He, J., Unifying theories of programming, (1998), Prentice-Hall
[2] Cavalcanti, A.; Woodcock, J., A tutorial introduction to CSP in unifying theories of programming, (Refinement Techniques in Software Engineering, Lect. Notes Comput. Sci., vol. 3167, (2006), Springer), 220-268
[3] Hoare, C. A.R., Communicating sequential processes, (1985), Prentice-Hall · Zbl 0637.68007
[4] Bergstra, J. A.; Klop, J. W., Process algebra for synchronous communication, Inf. Control, 60, 1-3, 109-137, (1984) · Zbl 0597.68027
[5] Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008
[6] Oliveira, M.; Cavalcanti, A.; Woodcock, J., A UTP semantics for circus, Form. Asp. Comput., 21, 3-32, (2009) · Zbl 1165.68048
[7] Wei, K.; Woodcock, J.; Cavalcanti, A., circus time with reactive designs, (Unifying Theories of Programming, Lect. Notes Comput. Sci., vol. 7681, (2013), Springer), 68-87 · Zbl 1452.68057
[8] Foster, S.; Thiele, B.; Cavalcanti, A.; Woodcock, J., Towards a UTP semantics for modelica, (Proc. 6th Intl. Symp. on Unifying Theories of Programming, Lect. Notes Comput. Sci., vol. 10134, (2016), Springer), 44-64 · Zbl 06700457
[9] He, J., From CSP to hybrid systems, (Roscoe, A. W., A Classical Mind: Essays in Honour of C. A. R. Hoare, (1994), Prentice Hall), 171-189
[10] Foster, S.; Zeyda, F.; Woodcock, J., Unifying heterogeneous state-spaces with lenses, (Proc. 13th Intl. Conf. on Theoretical Aspects of Computing (ICTAC), Lect. Notes Comput. Sci., vol. 9965, (2016), Springer), 295-314 · Zbl 06667713
[11] Smith, M., A unifying theory of true concurrency based on CSP and lazy observation, (Communicating Process Architectures, (2005), IOS Press), 177-188
[12] Zhu, L.; Xu, Q.; He, J.; Zhu, H., A formal model for a hybrid programming language, (Naumann, D., UTP, Lect. Notes Comput. Sci., vol. 8963, (2014), Springer), 125-142 · Zbl 1457.68038
[13] Woodcock, J., Engineering utopia - formal semantics for CML, (FM 2014: Formal Methods, Lect. Notes Comput. Sci., vol. 8442, (2014), Springer), 22-41
[14] Lee, E. A., Constructive models of discrete and continuous physical phenomena, IEEE Access, 2, 797-821, (2014)
[15] Hayes, I. J.; Dunne, S. E.; Meinicke, L., Unifying theories of programming that distinguish nontermination and abort, (Mathematics of Program Construction (MPC), Lect. Notes Comput. Sci., vol. 6120, (2010), Springer), 178-194 · Zbl 1286.68079
[16] Hayes, I., Termination of real-time programs: definitely, definitely not, or maybe, (Dunne, S.; Stoddart, B., Proc. 1st Intl. Symp. on Unifying Theories of Programming, Lect. Notes Comput. Sci., vol. 4010, (2006), Springer), 141-154 · Zbl 1186.68087
[17] Höfner, P.; Möller, B., An algebra of hybrid systems, J. Log. Algebraic Program., 78, 2, 74-97, (2009) · Zbl 1161.68032
[18] Armstrong, A.; Gomes, V.; Struth, G., Building program construction and verification tools from algebraic principles, Form. Asp. Comput., 28, 2, 265-293, (2015) · Zbl 1342.68066
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.