Formally Verified Animation for RoboChart Using Interaction Trees

TY - GEN

T1 - Formally Verified Animation for RoboChart Using Interaction Trees

AU - Ye, Kangfeng

AU - Foster, Simon

AU - Woodcock, Jim

N1 - This work is funded by the EPSRC projects CyPhyAssure (Grant EP/S001190/1), RoboCalc (Grant EP/M025756/1), and RoboTest (Grant EP/R025479/1). The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from www.flaticon. com, and are licensed under CC 3.0 BY. © Springer Nature Switzerland AG 2022. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

PY - 2022/10/10

Y1 - 2022/10/10

N2 - RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has a formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisations of ITrees along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this paper, we use ITrees to give RoboChart a novel operational semantics, implement it in Isabelle, and use Isabelle’s code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.

AB - RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has a formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisations of ITrees along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this paper, we use ITrees to give RoboChart a novel operational semantics, implement it in Isabelle, and use Isabelle’s code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.

KW - Interaction Trees

KW - CSP

KW - Theorem proving

KW - RoboChart

KW - Code Generation

KW - Robotic software

KW - Operational semantics

UR - http://www.scopus.com/inward/record.url?scp=85141709741&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-17244-1_24

DO - 10.1007/978-3-031-17244-1_24

M3 - Conference contribution

AN - SCOPUS:85141709741

SN - 9783031172434

T3 - Lecture Notes in Computer Science

SP - 404

EP - 420

BT - Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Proceedings

A2 - Riesco, Adrian

A2 - Zhang, Min

PB - Springer

T2 - 23rd International Conference on Formal Engineering Methods, ICFEM 2022

Y2 - 24 October 2022 through 27 October 2022

ER -