Probabilistic modelling and verification using RoboChart and PRISM

RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The ex...

Full description

Saved in:
Bibliographic Details
Published in:Software and systems modeling 2022-04, Vol.21 (2), p.667-716
Main Authors: Ye, Kangfeng, Cavalcanti, Ana, Foster, Simon, Miyazawa, Alvaro, Woodcock, Jim
Format: Article
Language:English
Subjects:
Automation
Compilers
Computer Science
Control algorithms
Domain specific languages
Information Systems Applications (incl.Internet)
Interpreters
IT in Business
Language
Modelling
Probabilistic models
Programming Languages
Programming Techniques
Regular Paper
Robotics
Robots
Semantics
Software Engineering
Software Engineering/Programming and Operating Systems
State machines
Statistical analysis
Temporal logic
Uncertainty
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.
ISSN:1619-1366
1619-1374
DOI:10.1007/s10270-021-00916-8