Paper Info
Title
Verified simulation for robotics.
Abstract
Simulation is a favoured technique for analysis of robotic systems. Currently, however, simulations are programmed in an ad hoc way, for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-level language is used, no clear relation between the simulation and a design model is established. We describe a tool-independent notation called RoboSim, designed specifically for modelling of (verified) simulations. We describe the syntax, well-formedness conditions, and semantics of RoboSim. We also show how we can use RoboSim models to check if a simulation is consistent with a functional design written in a UML-like notation akin to those often used by practitioners on an informal basis. We show how to check whether the design enables a feasible scheduling of behaviours in cycles as needed for a simulation, and formalise implicit assumptions routinely made when programming simulations. We develop a running example and three additional case studies to illustrate RoboSim and the proposed verification techniques. Tool support is also briefly discussed. Our results enable the description of simulations using tool-independent diagrammatic models amenable to verification and automatic generation of code.
Year
DOI
Venue
2019
10.1016/j.scico.2019.01.004
Science of Computer Programming
Keywords
Field
DocType
State machines,Process algebra,CSP,Semantics,Refinement
Robotic systems,Notation,Programming language,Diagrammatic reasoning,Computer science,Scheduling (computing),Functional design,Artificial intelligence,Syntax,Robotics,Semantics
Journal
Volume
ISSN
Citations 
174
0167-6423
1
PageRank 
References 
Authors
0.41
24
8
Name
Order
Citations
PageRank
Ana Cavalcanti166859.95
Augusto Sampaio250143.38
Alvaro Miyazawa3919.33
Pedro Ribeiro4184.74
Madiel Conserva Filho521.46
André Didier6173.07
Wei Li 00557614.16
Jon Timmis81237120.32