Browse by author
Lookup NU author(s): Professor Michael HarrisonORCiD
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
© Formal Methods for Interactive Systems 2013. This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.
Author(s): Harrison MD, Masci P, Campos JC, Curzon P
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013)
Year of Conference: 2013
Publisher: Universitatsbibliothek TU Berlin
URL: https://doi.org/10.14279/tuj.eceasst.69.962.943
DOI: 10.14279/tuj.eceasst.69.962.943
Series Title: Electronic Communications of the EASST
