More Web Proxy on the site http://driver.im/

Article

Using coupled simulations in non-atomic refinement

Authors:

Heike WehrheimAuthors Info & Claims

ZB'03: Proceedings of the 3rd international conference on Formal specification and development in Z and B

Pages 127 - 147

Published: 04 June 2003 Publication History

Abstract

Refinement is one of the most important techniques in formal system design, supporting stepwise development of systems from abstract specifications into more concrete implementations. Nonatomic refinement is employed when the level of granularity changes during a refinement step, i.e., whenever an abstract operation is refined into a sequence of concrete operations, as opposed to a single concrete operation. There has been some limited work on non-atomic refinement in Z, and the purpose of this paper is to extend this existing theory. In particular, we strengthen the proposed definition to exclude certain behaviours which only occur in the concrete specification but have no counterpart on the abstract level. To do this we use coupled simulations: the standard simulation relation is complemented by a second relation which guarantees the exclusion of undesired behaviour of the concrete system. These two relations have to agree at specific points (coupling condition), thus ensuring the desired close correspondence between abstract and concrete specification.

References

[1]

J.-R. Abrial. The B-Book: Assigning Programs to Meanings. CUP, 1996.

Digital Library

[2]

L. Aceto. Action Refinement in Process Algebras. CUP, London, 1992.

Digital Library

[3]

L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Information and Computation, 103:204-269, 1993.

Digital Library

[4]

E. A. Boiten and J. Derrick. IO-refinement in Z. In A. Evans, D. J. Duke, and T. Clark, editors, 3rd BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, September 1998. http://www.ewic.org.uk/.

Digital Library

[5]

W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. CUP, 1998.

Digital Library

[6]

J. Derrick and E. Boiten. Non-atomic refinement in Z. In J. Woodcock and J. Wing, editors, FM'99, World Congress on Formal Methods, number 1709 in LNCS, pages 1477-1496. Springer, 1999.

Digital Library

[7]

J. Derrick and E. A. Boiten. Refinement in Z and Object-Z. Springer-Verlag, 2001.

Digital Library

[8]

C. Fischer. CSP-OZ - a combination of CSP and Object-Z. In H. Bowman and J. Derrick, editors, Second IFIP International conference on Formal Methods for Open Object-based Distributed Systems, pages 423-438. Chapman & Hall, July 1997.

Digital Library

[9]

C. Fischer. How to combine Z with a process algebra. In ZUM'98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 5-23. Springer-Verlag, September 1998.

Digital Library

[10]

C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

Digital Library

[11]

C. B. Jones. Systematic Software Development using VDM. Prentice Hall, 1989.

Digital Library

[12]

J. Parrow and P. Sjödin. Multiway Synchronisation Verified with Coupled Simulation. In R. Cleaveland, editor, CONCUR '92, Concurrency Theory, number 630 in LNCS, pages 518-533. Springer, 1992.

Digital Library

[13]

A. Rensink. Action Contraction. In C. Palamidessi, editor, CONCUR 2000 - Concurrency Theory, number 1877 in LNCS, pages 290-304. Springer, 2000.

Digital Library

[14]

A. Rensink and R. Gorrieri. Action refinement as an implementation relation. In M. Bidoit and M. Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 772-786, 1997.

Digital Library

[15]

G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME'97: Industrial Application and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science, pages 62-81. Springer-Verlag, September 1997.

Digital Library

[16]

G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design, 18:249-284, May 2001.

Digital Library

[17]

J. M. Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice Hall, 2nd edition, 1992.

Digital Library

[18]

S. Stepney, D. Cooper, and J. C. P. Woodcock. More powerful data refinement in Z. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM'98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 284-307. Springer-Verlag, September 1998.

Digital Library

[19]

H. Treharne and S. Schneider. Using a process algebra to control B operations. In K. Araki, A. Galloway, and K. Taguchi, editors, International Conference on Integrated Formal Methods 1999 (IFM'99), pages 437-456, York, July 1999. Springer.

Digital Library

[20]

R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, volume 379 of LNCS, pages 237-248. Springer, 1989.

Digital Library

[21]

Walter Vogler. Failure semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139-162, 1991.

Digital Library

[22]

J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.

Digital Library

Cited By

Dongol BDerrick J(2015)Verifying LinearisabilityACM Computing Surveys10.1145/279655048:2(1-43)Online publication date: 24-Sep-2015
https://dl.acm.org/doi/10.1145/2796550
Derrick JDongol BSchellhorn GTofan BTravkin OWehrheim H(2014)Quiescent ConsistencyProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_15(200-214)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_15
Derrick JSchellhorn GWehrheim H(2011)Mechanically verified proof obligations for linearizabilityACM Transactions on Programming Languages and Systems10.1145/1889997.189000133:1(1-43)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.1145/1889997.1890001
Show More Cited By

Recommendations

Full Abstractness of a Metric Semantics for Action Refinement

For a process language with action refinement and synchronization both an operational and a denotational semantics are given. The operational semantics is based on an SOS-style transition system specification involving syntactical refinement sequences. ...
Event-based operational semantics and a consistency result for real-time concurrent processes with action refinement
Abstract
In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The ...
Introducing extra operations in refinement
Abstract
This paper reconsiders refinements which introduce actions on the concrete level which were not present at the abstract level. It considers a range of different basic refinement relations, covering the standard ones for formalisms like Event-B, Z, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ZB'03: Proceedings of the 3rd international conference on Formal specification and development in Z and B

June 2003

546 pages

ISBN:3540402535

Editors:
Didier Bert
CNRS, Laboratoire LSR-IMAG, Saint-Martin-d'Heres Cedex, France
,
Jonathan P. Bowen
London South Bank University, London, UK
,
Steve King
University of York, Department of Computer Science, Heslington, York, UK
,
Marina Waldén
Åbo Akademi University, Department of Computer Science, Turku, Finland

Sponsors

FME
Z User Group
Nokia
ClearSy System Engineering
BCS-FACS

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 04 June 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dongol BDerrick J(2015)Verifying LinearisabilityACM Computing Surveys10.1145/279655048:2(1-43)Online publication date: 24-Sep-2015
https://dl.acm.org/doi/10.1145/2796550
Derrick JDongol BSchellhorn GTofan BTravkin OWehrheim H(2014)Quiescent ConsistencyProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_15(200-214)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_15
Derrick JSchellhorn GWehrheim H(2011)Mechanically verified proof obligations for linearizabilityACM Transactions on Programming Languages and Systems10.1145/1889997.189000133:1(1-43)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.1145/1889997.1890001
Schellhorn GGrandy HHaneberg DMoebius NReif W(2009)A systematic verification approach for mondex electronic purses using ASMsRigorous Methods for Software Construction and Analysis10.5555/2172244.2172251(93-110)Online publication date: 1-Jan-2009
https://dl.acm.org/doi/10.5555/2172244.2172251
Schneider STreharne H(2009)Changing System Interfaces ConsistentlyProceedings of the 7th International Conference on Integrated Formal Methods10.1007/978-3-642-00255-7_8(103-117)Online publication date: 16-Feb-2009
https://dl.acm.org/doi/10.1007/978-3-642-00255-7_8
Schellhorn G(2008)Refinement of State-Based SystemsProceedings of the 1st international conference on Abstract State Machines, B and Z10.1007/978-3-540-87603-8_4(39-41)Online publication date: 16-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-87603-8_4
Derrick JSchellhorn GWehrheim H(2008)Mechanizing a Correctness Proof for a Lock-Free Concurrent StackProceedings of the 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems10.1007/978-3-540-68863-1_6(78-95)Online publication date: 4-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-68863-1_6
Haneberg DGrandy HReif WSchellhorn G(2007)Verifying smart card applicationsProceedings of the 6th international conference on Integrated formal methods10.5555/1770498.1770515(313-332)Online publication date: 2-Jul-2007
https://dl.acm.org/doi/10.5555/1770498.1770515
Derrick JSchellhorn GWehrheim H(2007)Proving linearizability via non-atomic refinementProceedings of the 6th international conference on Integrated formal methods10.5555/1770498.1770509(195-214)Online publication date: 2-Jul-2007
https://dl.acm.org/doi/10.5555/1770498.1770509
Derrick JWehrheim H(2005)Non-atomic refinement in z and CSPProceedings of the 4th international conference on Formal Specification and Development in Z and B10.1007/11415787_3(24-44)Online publication date: 13-Apr-2005
https://dl.acm.org/doi/10.1007/11415787_3
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents