Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Foundations for using linear temporal logic in Event-B refinement
Hoang T., Schneider S., Treharne H., Williams D. Formal Aspects of Computing28 (6):909-935,2016.Type:Article
Date Reviewed: Apr 12 2017

Event-B is a formal method for system-level modeling and analysis. In the last decade, Event-B refinement has generated a lot of interest as a formalism for developing highly reliable software. The Event-B language, along with tools such as Rodin and ProB, provides a pragmatic environment for software development.

One of the early criticisms of Event-B was the lack of a clear semantic basis for the refinement process at the level of a system. Event-B focused on the notion of refinement of each individual event, but the meaning of refinement at the level of the entire system was not clearly spelled out. This was compounded by the fact that Event-B used a different notion of refinement than B (or Z)--pre-condition strengthening instead of pre-condition weakening. This was presumably to treat the refinement of traces of events.

Event-B also allowed the introduction of new events, and splitting existing events during refinement--this complicated the question of semantics of refinement at the system level. This criticism has since been addressed quite effectively by providing a semantics of refinement using formalisms like CSP and Unity to deal with traces generated by an Event-B machine.

Given the ability to reason about traces, the natural question that arises is about the interaction of temporal logics with the refinement process. This paper is the latest in a series of efforts to answer this question.

The authors build on previous work where they showed that refinement preserves LTL properties under some conditions--some of which were not very intuitive (β-dependency). In this paper, the authors show a much more natural result, and also include a larger subset of the logic that is capable of expressing enable-predicates.

An interesting aspect is that results do not hold for every step of refinement; rather, they hold for a sequence of refinement steps that end with a model that satisfies certain semantic conditions (deadlock freedom, and absence of anticipated events). This seems to be a pragmatic approach, but it remains to be seen whether this approach will enable new refinement strategies that include temporal properties in Event-B.

Reviewer:  Prahladavaradan Sampath Review #: CR145189 (1706-0386)
Bookmark and Share
 
Mechanical Verification (F.3.1 ... )
 
 
Methodologies (D.2.10 ... )
 
 
Temporal Logic (F.4.1 ... )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Mechanical Verification": Date
Fast automatic liveness analysis of hierarchical parallel systems
Rohrich J.  Programming Languages and System Design (, Dresden, East Germany,271983. Type: Proceedings
Feb 1 1985
Mechanical proofs about computer programs
Good D.  Mathematical logic and programming languages (, London, UK,751985. Type: Proceedings
Feb 1 1986
The characterization problem for Hoare logics
Clarke E.  Mathematical logic and programming languages (, London, UK,1061985. Type: Proceedings
Jun 1 1986
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy