By the same authors

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

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

Standard

Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. / Foster, Simon David; Baxter, James Edward; Cavalcanti, Ana Lucia Caneca; Miyazawa, Alvaro Heiji; Woodcock, JAMES Charles Paul.

15th International Conference on Formal Aspects of Component Software. ed. / Peter Csaba Ölveczky; Kyungmin Bae. Springer, 2018. p. 137-155 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11222 LNCS).

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

Harvard

Foster, SD, Baxter, JE, Cavalcanti, ALC, Miyazawa, AH & Woodcock, JAMESCP 2018, Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. in PC Ölveczky & K Bae (eds), 15th International Conference on Formal Aspects of Component Software. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11222 LNCS, Springer, pp. 137-155. https://doi.org/10.1007/978-3-030-02146-7_7

APA

Foster, S. D., Baxter, J. E., Cavalcanti, A. L. C., Miyazawa, A. H., & Woodcock, JAMES. C. P. (2018). Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In P. C. Ölveczky, & K. Bae (Eds.), 15th International Conference on Formal Aspects of Component Software (pp. 137-155). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11222 LNCS). Springer. https://doi.org/10.1007/978-3-030-02146-7_7

Vancouver

Foster SD, Baxter JE, Cavalcanti ALC, Miyazawa AH, Woodcock JAMESCP. Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In Ölveczky PC, Bae K, editors, 15th International Conference on Formal Aspects of Component Software. Springer. 2018. p. 137-155. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-02146-7_7

Author

Foster, Simon David ; Baxter, James Edward ; Cavalcanti, Ana Lucia Caneca ; Miyazawa, Alvaro Heiji ; Woodcock, JAMES Charles Paul. / Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. 15th International Conference on Formal Aspects of Component Software. editor / Peter Csaba Ölveczky ; Kyungmin Bae. Springer, 2018. pp. 137-155 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Bibtex - Download

@inproceedings{15fc8acdf5ba4b35adf5e5c097288a95,
title = "Automating Verification of State Machines with Reactive Designs and Isabelle/UTP",
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.",
keywords = "cs.LO",
author = "Foster, {Simon David} and Baxter, {James Edward} and Cavalcanti, {Ana Lucia Caneca} and Miyazawa, {Alvaro Heiji} and Woodcock, {JAMES Charles Paul}",
note = "{\textcopyright} This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details",
year = "2018",
month = oct,
day = "5",
doi = "10.1007/978-3-030-02146-7_7",
language = "English",
isbn = "9783030021450",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "137--155",
editor = "{\"O}lveczky, {Peter Csaba} and Kyungmin Bae",
booktitle = "15th International Conference on Formal Aspects of Component Software",

}

RIS (suitable for import to EndNote) - Download

TY - GEN

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

AU - Foster, Simon David

AU - Baxter, James Edward

AU - Cavalcanti, Ana Lucia Caneca

AU - Miyazawa, Alvaro Heiji

AU - Woodcock, JAMES Charles Paul

N1 - © 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 - 2018/10/5

Y1 - 2018/10/5

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

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

KW - cs.LO

U2 - 10.1007/978-3-030-02146-7_7

DO - 10.1007/978-3-030-02146-7_7

M3 - Conference contribution

SN - 9783030021450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 137

EP - 155

BT - 15th International Conference on Formal Aspects of Component Software

A2 - Ölveczky, Peter Csaba

A2 - Bae, Kyungmin

PB - Springer

ER -