Projects per year
Abstract
We outline a probabilistic denotational semantics for the RoboChart language, a diagrammatic, domain-specific notation for de- scribing robotic controllers with their hardware platforms and operating environments. We do this using a powerful (but perhaps not so well known) semantic technique: He, Morgan, and McIver’s weakest completion semantics, which is based on Hoare and He’s Unifying Theories of Programming. In this approach, we do the following: (1) start with the standard semantics for a nondeterministic programming language; (2) propose a new probabilistic semantic domain; (3) propose a forgetful function from the probabilistic semantic domain to the standard semantic domain; (4) use the converse of the forgetful function to embed the standard semantic domain in the probabilistic semantic domain; (5) demonstrate that this embedding preserves program structure; (6) define the probabilistic choice operator. Weakest completion semantics guides the semantic definition of new languages by building on existing semantics and, in this case, tackling a notoriously thorny issue: the relationship between demonic and probabilistic choice. Consistency ensures that programming intuitions, development techniques, and proof methods can be carried over from the standard language to the probabilistic one. We largely follow He et al., our contribution being an explication of the technique with meticulous proofs suitable for mechanisation in Isabelle/UTP.
Original language | English |
---|---|
Title of host publication | Unifying Theories of Programming |
Subtitle of host publication | 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings |
Editors | Pedro Ribeiro, Augusto Sampaio |
Publisher | Springer |
ISBN (Electronic) | 978-3-030-31038-7 |
ISBN (Print) | 978-3-030-31037-0 |
Publication status | Published - 4 Nov 2019 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 11885 |
Keywords
- RoboChart language
- Robotic controllers
- Statecharts
- Probabilistic semantics
- Relational calculus
- Unifying Theories of Programming (UTP)
- Weakest completion semantics
Projects
- 2 Finished
-
Requirements Modelling for Cyber-Physical Systems
31/03/18 → 30/09/20
Project: Research project (funded) › Research
-
A Calculus for Software Engineering of Mobile and Autonomous Robots
Cavalcanti, A. L. C., Timmis, J., Woodcock, J., Foster, S. D., Li, W., Miyazawa, A. & Ribeiro, P.
1/09/15 → 30/06/21
Project: Research project (funded) › Research