University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Foundations for using Linear Temporal Logic in Event-B refinement

Hoang, TS, Schneider, SA, Treharne, H and Williams, DM (2016) Foundations for using Linear Temporal Logic in Event-B refinement Formal Aspects of Computing, 28 (6). pp. 909-935.

[img]
Preview
Text
Foundations for using Linear.pdf - Version of Record
Available under License : See the attached licence file.

Download (985kB) | Preview
[img]
Preview
Text (licence)
SRI_deposit_agreement.pdf
Available under License : See the attached licence file.

Download (33kB) | Preview
[img] Text
Schneiderpaper.pdf - Accepted version Manuscript
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (393kB)

Abstract

In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.

Item Type: Article
Subjects : Computing Science
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
Hoang, TSUNSPECIFIEDUNSPECIFIED
Schneider, SAUNSPECIFIEDUNSPECIFIED
Treharne, HUNSPECIFIEDUNSPECIFIED
Williams, DMUNSPECIFIEDUNSPECIFIED
Date : November 2016
Identification Number : 10.1007/s00165-016-0376-0
Copyright Disclaimer : © The Author(s) 2016. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
Uncontrolled Keywords : Event-B, Refinement, Linear Temporal Logic
Depositing User : Symplectic Elements
Date Deposited : 13 Jul 2016 16:52
Last Modified : 29 Sep 2016 11:53
URI: http://epubs.surrey.ac.uk/id/eprint/811208

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800