Edinburgh Research Explorer

Extending the Dafny IDE with tactics and dead annotation analysis (tool demo)

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

  • Gudmund Grov
  • Yuhui Lin
  • Léon McGregor
  • Vytautas Tumas
  • Duncan Cameron

Related Edinburgh Organisations

Open Access permissions

Open

Original languageEnglish
Title of host publicationProceedings of the Third Workshop on Formal Integrated Development Environment
PublisherOpen Publishing Association
StatePublished - 8 Nov 2016

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume240
ISSN (Electronic)2075-2180

Abstract

We are concerned with systems, particularly safety-critical systems, that involve interaction between users and devices, such as the user interface of medical devices. We therefore developed a MISRA C code generator for formal models expressed in the PVSio-web prototyping toolkit. PVSio-web allows developers to rapidly generate realistic interactive prototypes for verifying usability and safety requirements in human-machine interfaces. The visual appearance of the prototypes is based on a picture of a physical device, and the behaviour of the prototype is defined by an executable formal model. Our approach transforms the PVSio-web prototyping tool into a model-based engineering toolkit that, starting from a formally verified user interface design model, will produce MISRA C code that can be compiled and linked into a final product. An initial validation of our tool is presented for the data entry system of an actual medical device.

ID: 41133271