English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

RoboChart is a core notation in the RoboStar framework. It is a timed andprobabilistic domain-specific and state machine-based language for robotics.RoboChart supports shared variables and communication across entities in itscomponent model. It has formal denotational semantics given in CSP. Thesemantic technique of Interaction Trees (ITrees) represents behaviours ofreactive and concurrent programs interacting with their environments. Recentmechanisation of ITrees, along with ITree-based CSP semantics and a Zmathematical toolkit in Isabelle/HOL, bring new applications of verificationand animation for state-rich process languages, such as RoboChart. In thispaper, we use ITrees to give RoboChart novel operational semantics, implementit in Isabelle, and use Isabelle's code generator to generate verified andexecutable animations. We illustrate our approach using an autonomous chemicaldetector model and a patrol robot model additionally exhibiting nondeterminismand using shared variables. With animation, we show two concrete scenarios forthe chemical detector when the robot encounters different environmental inputsand three concrete scenarios for the patrol robot when its calibrated positionis in different sections of a corridor. We also verify that the animatedscenarios are truly trace refinements of the CSP denotational semantics of theRoboChart models using FDR, a refinement model checker for CSP. This ensuresthat our approach to resolving nondeterminism using CSP operators with priorityis sound and correct.

Formally Verified Animation for RoboChart using Interaction Trees