By the same authors

Automating Verification of State Machines with Reactive Designs and Isabelle/UTP

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Department/unit(s)

Publication details

Title of host publication15th International Conference on Formal Aspects of Component Software
DateAccepted/In press - 8 Aug 2018
DatePublished (current) - 5 Oct 2018
Pages137-155
Number of pages18
PublisherSpringer
EditorsPeter Csaba Ölveczky, Kyungmin Bae
Original languageEnglish
ISBN (Print)9783030021450

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11222 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Abstract

State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.

Bibliographical note

© 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

    Research areas

  • cs.LO

Research outputs

  • RoboTool

    Research output: Non-textual formSoftware

Activities

Projects

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations