By the same authors

Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

Research output: Working paper

Full text download(s)

Links

Author(s)

Department/unit(s)

Publication details

DatePublished - 14 May 2019
Original languageEnglish

Publication series

NamearXiv

Abstract

The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantic models. These can be further applied in the development of verification tools, harnessing Isabelle/HOL's powerful proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, including algebraic and axiomatic semantics, and UTP theories to encode computational paradigms. We illustrate our approach with a variety of proof tools, and in particular develop a verification tool for the formal state machine notation, RoboChart.

Bibliographical note

45 pages, submitted to Science of Computer Programming, March 2019

    Research areas

  • cs.LO, cs.FL

Activities

Discover related content

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

View graph of relations