Detailed description of the files in this directory Jump to my home page Jump to Bart Jacobs home page Download the distribution Download the paper "Assertional and Behavioural Refinement in Coalgebraic Specification.

Assertional and Behavioural Refinement in Coalgebraic Specification

This page describes the CCSL and PVS sources of the Transaction-Commit example of Section 6 of our paper "Assertional and Behavioural Refinement in Coalgebraic Specification".

General Information

Abstract of the paper

Refinements between specifications in a coalgebraic setting have been introduced in [1,2]. This paper presents a renewed, extended study of refinements, based on more practical experience. It distinguishes assertional refinement (assertions should be valid, after translation) and behavioural refinement (appropriate behaviour must be simulated, after translation). Behavioural refinement is the more general notion, it offers greater flexibility, especially in the presence of non-public methods. Assertional refinement is shown to be a special case of behavioural refinement. The (coalgebraic) notions of invariant and bisimulation will be essential in these investigations. In the end, refinement in a coalgebraic setting is illustrated via two refinements of an abstract transaction-commit mechanism.

About the contents of this directory

Transaction are used to make certain designated sequences of actions atomic. Transaction mechanism are important in the context of databases or operating systems, but also in the world of smart cards --- where there is always the possibility that a smart card is removed before an appropriate sequence of actions is completed, see Chapter 5 of [3]. In the Section 5 of our paper we give an abstract specification of a (simplified) transaction mechanism in the CCSL. There are two standard implementation techniques for a transaction mechanism: new value logging and old value logging. For both we develop a CCSL specification and prove in PVS that they refine the abstract specification. Besides that we developed models of all specification in PVS, thus showing that the specifications are consistent. Further, there are a number of lemmas that describe abstract properties of the specifications. Among them there is also the PVS equivalent of Lemma 7.1 from the paper.

The complete sources, including all proofs, are available by following one of the links above or below.

Technicalities

The refinement proofs have been developed with PVS 2.3 patch level 1.2.2.36. To typecheck everything start PVS in this directory and type
M-x load-file typechek.el
You can prove everything by issuing prove-importchain in theory top, file all.pvs.

References

[1]
B. Jacobs, Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs. In M. Bidoit and M. Dauchet, editors, TAPSOFT'97: Theory and Practice of Software Development, LNCS number 1214, pages 787-802. Springer, Berlin, 1997. Online available at http://www.cwi.nl/~bjacobs/papers.html.
[2]
B. Jacobs, Invariants, Bisimulations and the Correctness of Coalgebraic Refinements. In: M. Johnson (ed), Algebraic Methodology and Software Technology, LNCS 1349, p.276-291. Springer, Berlin, 1997. Online available at http://www.cs.kun.nl/~bart/PAPERS/
[3]
Z. Chen, Java Card Technology for Smart Cards. The Java Series. Addison-Wesley, 2000.

Detailed description of the files in this directory Jump to my home page Jump to Bart Jacobs home page Download the distribution Download the paper "Assertional and Behavioural Refinement in Coalgebraic Specification.

last changed on 9 Aug 2001 by Hendrik