Foundations for using linear temporal logic in Event-B refinement

Thai Son Hoang, Steve Schneider, Helen Treharne, David Williams

Research output: Contribution to journalArticlepeer-review

17 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)909–935
JournalFormal Aspects of Computing
Volume28
Issue number6
Early online date27 Apr 2016
DOIs
Publication statusPublished - 1 Nov 2016
Externally publishedYes

Keywords

  • Event-B
  • Refinement
  • Linear Temporal Logic

Fingerprint

Dive into the research topics of 'Foundations for using linear temporal logic in Event-B refinement'. Together they form a unique fingerprint.

Cite this