Analysing RoboChart with probabilities

M. S. Conserva Filho*, R. Marinho, A. Mota, J. Woodcock

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationFormal Methods
Subtitle of host publicationFoundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings
EditorsTiago Massoni, Mohammad Reza Mousavi
PublisherSpringer
Pages198-214
Number of pages17
ISBN (Print)9783030030438
DOIs
Publication statusE-pub ahead of print - 24 Oct 2018
Event21st Brazilian Symposium on Formal Methods, SBMF 2018 - Salvador, Brazil
Duration: 26 Nov 201830 Nov 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11254 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st Brazilian Symposium on Formal Methods, SBMF 2018
Country/TerritoryBrazil
CitySalvador
Period26/11/1830/11/18

Bibliographical note

© Springer Nature Switzerland AG 2018

Keywords

  • CSP
  • PRISM
  • Probabilistic analysis
  • Robotic systems

Cite this