Formally verified animation for RoboChart using interaction trees

DOI10.1016/J.JLAMP.2023.100940MaRDI QIDQ6151624zbMATH OpenFDO

Authors Kangfeng Ye, Simon Foster, Jim Woodcock

Publication date 12 February 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2303.09106

zbMATH Keywords

animation of robot softwarecode generationCSPinteraction treesoperational semanticstheorem proving

Mathematics Subject Classification ID

Computer science (68-XX)

Abstract: 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 formal denotational semantics given in CSP. The semantic technique of Interaction Trees (ITrees) represents behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation 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 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 and a patrol robot model additionally exhibiting nondeterminism and using shared variables. With animation, we show two concrete scenarios for the chemical detector when the robot encounters different environmental inputs and three concrete scenarios for the patrol robot when its calibrated position is in different sections of a corridor. We also verify that the animated scenarios are truly trace refinements of the CSP denotational semantics of the RoboChart models using FDR, a refinement model checker for CSP. This supports the soundness of our approach that the use of CSP operators with priority resolves nondeterminism correctly.

Cites work

• A Theory of Communicating Sequential Processes
• An overview of the K semantic framework
• Automated reasoning for probabilistic sequential programs with theorem proving
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Higher-order rewrite systems and their confluence
• scientific article; zbMATH DE number 3854137 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• scientific article; zbMATH DE number 7730622 (Why is no real title available?)
• Probabilistic semantics for RoboChart. A weakest completion approach
• The weakest prespecification
• Types for Proofs and Programs

This page was built for publication: Formally verified animation for RoboChart using interaction trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6151624)