Activities per year
Abstract
Robotic systems have applications in many real-life scenarios, ranging from household cleaning to critical operations. RoboChart is a graphical language for describing robotic controllers designed specifically for autonomous and mobile robots, providing architectural constructs to identify the requirements for a robotic platform. It also provides a formal semantics in CSP. RoboChart has a probabilistic operator (P) but no associated probabilistic CSP semantics. When (P) is used, currently a non-deterministic choice (Π) is used as semantics; this is a conservative semantics but it does not allow the analysis of stochastic properties. In this paper we define the semantics of the operator in terms of the probabilistic CSP operator ⊞. We also show how this augmented CSP semantics for RoboChart can be translated into the PRISM probabilistic language to be able to check stochastic properties.
Original language | English |
---|---|
Title of host publication | Formal Methods |
Subtitle of host publication | Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings |
Editors | Tiago Massoni, Mohammad Reza Mousavi |
Publisher | Springer |
Pages | 198-214 |
Number of pages | 17 |
ISBN (Print) | 9783030030438 |
DOIs | |
Publication status | E-pub ahead of print - 24 Oct 2018 |
Event | 21st Brazilian Symposium on Formal Methods, SBMF 2018 - Salvador, Brazil Duration: 26 Nov 2018 → 30 Nov 2018 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11254 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 21st Brazilian Symposium on Formal Methods, SBMF 2018 |
---|---|
Country/Territory | Brazil |
City | Salvador |
Period | 26/11/18 → 30/11/18 |
Bibliographical note
© Springer Nature Switzerland AG 2018Keywords
- CSP
- PRISM
- Probabilistic analysis
- Robotic systems
Activities
- 1 Seminar/workshop/course
-
Workshop on Requirements Modelling for Cyber-Physical Systems
Jim Woodcock (Advisor)
22 Jul 2019 → 24 Jul 2019Activity: Participating in or organising an event › Seminar/workshop/course
Projects
- 1 Finished
-
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