By the same authors

From the same journal

From the same journal

Verified simulation for robotics

Research output: Contribution to journalArticle

Standard

Verified simulation for robotics. / Cavalcanti, Ana; Sampaio, Augusto; Miyazawa, Alvaro; Ribeiro, Pedro; Filho, Madiel Conserva; Didier, André; Li, Wei; Timmis, Jon.

In: Science of Computer Programming, 11.01.2019.

Research output: Contribution to journalArticle

Harvard

Cavalcanti, A, Sampaio, A, Miyazawa, A, Ribeiro, P, Filho, MC, Didier, A, Li, W & Timmis, J 2019, 'Verified simulation for robotics', Science of Computer Programming. https://doi.org/10.1016/j.scico.2019.01.004

APA

Cavalcanti, A., Sampaio, A., Miyazawa, A., Ribeiro, P., Filho, M. C., Didier, A., ... Timmis, J. (2019). Verified simulation for robotics. Science of Computer Programming. https://doi.org/10.1016/j.scico.2019.01.004

Vancouver

Cavalcanti A, Sampaio A, Miyazawa A, Ribeiro P, Filho MC, Didier A et al. Verified simulation for robotics. Science of Computer Programming. 2019 Jan 11. https://doi.org/10.1016/j.scico.2019.01.004

Author

Cavalcanti, Ana ; Sampaio, Augusto ; Miyazawa, Alvaro ; Ribeiro, Pedro ; Filho, Madiel Conserva ; Didier, André ; Li, Wei ; Timmis, Jon. / Verified simulation for robotics. In: Science of Computer Programming. 2019.

Bibtex - Download

@article{d81a25876f5f496ea948de41358d958b,
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.",
keywords = "State machines, Process algebra, CSP, Semantics, Refinement",
author = "Ana Cavalcanti and Augusto Sampaio and Alvaro Miyazawa and Pedro Ribeiro and Filho, {Madiel Conserva} and Andr{\'e} Didier and Wei Li and Jon Timmis",
note = "{\circledC} 2019 Elsevier B.V. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.",
year = "2019",
month = "1",
day = "11",
doi = "10.1016/j.scico.2019.01.004",
language = "English",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",

}

RIS (suitable for import to EndNote) - Download

TY - JOUR

T1 - Verified simulation for robotics

AU - Cavalcanti, Ana

AU - Sampaio, Augusto

AU - Miyazawa, Alvaro

AU - Ribeiro, Pedro

AU - Filho, Madiel Conserva

AU - Didier, André

AU - Li, Wei

AU - Timmis, Jon

N1 - © 2019 Elsevier B.V. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

PY - 2019/1/11

Y1 - 2019/1/11

N2 - 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.

AB - 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.

KW - State machines, Process algebra, CSP, Semantics, Refinement

U2 - 10.1016/j.scico.2019.01.004

DO - 10.1016/j.scico.2019.01.004

M3 - Article

JO - Science of Computer Programming

T2 - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -