Journal
SOFTWARE AND SYSTEMS MODELING
Volume 21, Issue 2, Pages 667-716Publisher
SPRINGER HEIDELBERG
DOI: 10.1007/s10270-021-00916-8
Keywords
State machines; Formal semantics; Model transformation; PRISM; Probabilistic model checking; Domain-specific language for robotics
Categories
Funding
- EPSRC [EP/M025756/1, EP/R025479/1]
- Royal Academy of Engineering [CiET1718/45]
- EPSRC [EP/R025479/1, EP/M025756/1] Funding Source: UKRI
Ask authors/readers for more resources
RoboChart is a domain-specific language for robotics that supports automated verification through model checking and theorem proving, with an extension to model uncertainty using probabilism. The language includes a new construct for enriching state machines with probability and an accompanying tool called RoboTool for modelling and verifying functional and real-time behavior. An automatic technique has been implemented in RoboTool to transform RoboChart models into PRISM models for verification, with an extension of the property language to support probabilistic properties expressed in temporal logic using controlled natural language.
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available