ASM refinement and generalizations of forward simulation in data refinement: a comparison. (English) Zbl 1080.68058
Summary: In [J. Universal Comput. Sci. 7, 952–979 (2001)], we have formalized Börger’s refinement notion for Abstract State Machines (ASMs). The formalization was based on transition systems and verification conditions were expressed in Dynamic Logic.
In this paper, the relation between ASM refinement and data refinement is explored. Data refinement expresses operations and verification conditions using relational calculus.
We show how to bridge the gap between the different notations, and that forward simulation in the behavioral approach to data refinement can be viewed as a specific instance of ASM refinement with 1:1 diagrams, where control structure is not refined.
We also prove that two recent generalizations of data refinement, weak refinement and coupled refinement can be derived from ASM refinement.
In this paper, the relation between ASM refinement and data refinement is explored. Data refinement expresses operations and verification conditions using relational calculus.
We show how to bridge the gap between the different notations, and that forward simulation in the behavioral approach to data refinement can be viewed as a specific instance of ASM refinement with 1:1 diagrams, where control structure is not refined.
We also prove that two recent generalizations of data refinement, weak refinement and coupled refinement can be derived from ASM refinement.
MSC:
| 68Q45 | Formal languages and automata |
References:
| [1] | Abrial, J.-R., The B-BookAssigning Programs to Meanings (1996), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0915.68015 |
| [2] | N. Bjørner, A. Brown, M. Colon, B. Finkbeiner, Z. Manna, H. Sipma, T. Uribe, Verifying temporal properties of reactive systems: a step tutorial, in: Formal Methods in System Design, 2000, pp. 227-270.; N. Bjørner, A. Brown, M. Colon, B. Finkbeiner, Z. Manna, H. Sipma, T. Uribe, Verifying temporal properties of reactive systems: a step tutorial, in: Formal Methods in System Design, 2000, pp. 227-270. |
| [3] | E. Boiten, W. de Roever, Getting to the bottom of relational refinement: relations and correctness, partial and total (extended abstract), in: R. Berghammer, B. Möller (Eds.), 7th Intern. Seminar on Relational Methods in Computer Science (RelMCS 7), University of Kiel, 2003, pp. 82-88.; E. Boiten, W. de Roever, Getting to the bottom of relational refinement: relations and correctness, partial and total (extended abstract), in: R. Berghammer, B. Möller (Eds.), 7th Intern. Seminar on Relational Methods in Computer Science (RelMCS 7), University of Kiel, 2003, pp. 82-88. |
| [4] | C. Bolton, J. Davies, J. Woodcock, On the refinement and simulation of data types and processes, in: K. Araki, A. Galloway, K. Taguchi (Eds.), Proc. of the Intern. Conf. of Integrated Formal Methods (IFM), Springer, Berlin, 1999, pp. 273-292.; C. Bolton, J. Davies, J. Woodcock, On the refinement and simulation of data types and processes, in: K. Araki, A. Galloway, K. Taguchi (Eds.), Proc. of the Intern. Conf. of Integrated Formal Methods (IFM), Springer, Berlin, 1999, pp. 273-292. · Zbl 0963.68126 |
| [5] | E. Börger, A logical operational semantics for full prolog. Part I: selection core and control, in: E. Börger, H. Kleine Büning, M.M. Richter, W. Schönfeld (Eds.), CSL’89. 3rd Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1990, pp. 36-64.; E. Börger, A logical operational semantics for full prolog. Part I: selection core and control, in: E. Börger, H. Kleine Büning, M.M. Richter, W. Schönfeld (Eds.), CSL’89. 3rd Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1990, pp. 36-64. · Zbl 0925.68301 |
| [6] | E. Börger, A logical operational semantics of full prolog. Part II: Built-in predicates for database manipulation, in: B. Rovan (Ed.), Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 452, Springer, Berlin, 1990, pp. 1-14.; E. Börger, A logical operational semantics of full prolog. Part II: Built-in predicates for database manipulation, in: B. Rovan (Ed.), Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 452, Springer, Berlin, 1990, pp. 1-14. · Zbl 0796.68140 |
| [7] | Börger, E., The ASM refinement method, Formal Aspects of Computing, 15, 237-257 (2003) · Zbl 1093.68601 |
| [8] | Börger, E.; Rosenzweig, D., The WAM—definition and compiler correctness, (Beierle, C.; Plümer, L., Logic ProgrammingFormal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, Vol. 11 (1995), North-Holland: North-Holland Amsterdam), 20-90 · Zbl 0832.68024 |
| [9] | E. Börger, J. Schmid, Composition and submachine concepts for sequential ASMs, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic (Proc. of CSL 2000), Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 41-60.; E. Börger, J. Schmid, Composition and submachine concepts for sequential ASMs, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic (Proc. of CSL 2000), Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 41-60. · Zbl 0973.68066 |
| [10] | D. Cyrluk, Microprocessor verification in PVS: a methodology and simple example, Technical Report SRI-CSL-93-12, Computer Science Laboratory, SRI International, December 1993.; D. Cyrluk, Microprocessor verification in PVS: a methodology and simple example, Technical Report SRI-CSL-93-12, Computer Science Laboratory, SRI International, December 1993. |
| [11] | deBakker, J., Mathematical Theory of Program Correctness, (International Series in Computer Science (1980), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ) · Zbl 0452.68011 |
| [12] | de Roever, W.; Engelhardt, K., Data refinementmodel-oriented proof methods and their comparison, (Cambridge Tracts in Theoretical Computer Science, Vol. 47 (1998), Cambridge University Press: Cambridge University Press New York, NY) · Zbl 0955.68076 |
| [13] | J. Derrick, E. Boiten, Refinement in Z and in Object-Z : Foundations and Advanced Applications, FACIT, Springer, Berlin, 2001.; J. Derrick, E. Boiten, Refinement in Z and in Object-Z : Foundations and Advanced Applications, FACIT, Springer, Berlin, 2001. · Zbl 0982.68086 |
| [14] | J. Derrick, E. Boiten, Errata for Refinement in Z and in Object-Z : Foundations and Advanced Applications, FACIT, Springer, Berlin, 2001,; J. Derrick, E. Boiten, Errata for Refinement in Z and in Object-Z : Foundations and Advanced Applications, FACIT, Springer, Berlin, 2001, · Zbl 0982.68086 |
| [15] | J. Derrick, E. Boiten, Recent advances in refinement, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), ZB2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 33-56.; J. Derrick, E. Boiten, Recent advances in refinement, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), ZB2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 33-56. · Zbl 1021.68510 |
| [16] | J. Derrick, E.A. Boiten, H. Bowman, M. Steen, Weak refinement in Z, in: J. Bowen, M. Hinchey, D. Till (Eds.), ZUM ’97: The Z Formal Specification Notation, Lecture Notes in Computer Science, Vol. 1212, Springer, Berlin, 1997, pp. 369-388.; J. Derrick, E.A. Boiten, H. Bowman, M. Steen, Weak refinement in Z, in: J. Bowen, M. Hinchey, D. Till (Eds.), ZUM ’97: The Z Formal Specification Notation, Lecture Notes in Computer Science, Vol. 1212, Springer, Berlin, 1997, pp. 369-388. |
| [17] | J. Derrick, H. Wehrheim, Using coupled simulations in non-atomic refinement, in: D. Bert, J. Bowen, S. King, M. Walden (Eds.), ZB 2003: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 2651, Springer, Berlin, 2003, pp. 127-147.; J. Derrick, H. Wehrheim, Using coupled simulations in non-atomic refinement, in: D. Bert, J. Bowen, S. King, M. Walden (Eds.), ZB 2003: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 2651, Springer, Berlin, 2003, pp. 127-147. · Zbl 1028.68541 |
| [18] | A. Dold, A formal representation of abstract state machines using PVS, Verifix-Report Ulm 6.2, Universität Ulm (revised version), 1998.; A. Dold, A formal representation of abstract state machines using PVS, Verifix-Report Ulm 6.2, Universität Ulm (revised version), 1998. |
| [19] | Gurevich, M., Evolving algebras 1993Lipari guide, (Börger, E., Specification and Validation Methods (1995), Oxford University Press: Oxford University Press Oxford), 9-36 · Zbl 0852.68053 |
| [20] | He Jifeng, C.A.R. Hoare, J.W. Sanders, Data refinement refined, in: B. Robinet, R. Wilhelm (Eds.), Proc. ESOP 86, Lecture Notes in Computer Science, Vol. 213, Springer, Berlin, 1986, pp. 187-196.; He Jifeng, C.A.R. Hoare, J.W. Sanders, Data refinement refined, in: B. Robinet, R. Wilhelm (Eds.), Proc. ESOP 86, Lecture Notes in Computer Science, Vol. 213, Springer, Berlin, 1986, pp. 187-196. · Zbl 0587.68018 |
| [21] | Jones, C. B., Systematic Software Development using VDM (1990), Prentice-Hall: Prentice-Hall Englwood Cliffs, NJ · Zbl 0743.68048 |
| [22] | L. Lamport, The temporal logic of actions, ACM Trans. Programming Languages Systems 16 (3) (1994).; L. Lamport, The temporal logic of actions, ACM Trans. Programming Languages Systems 16 (3) (1994). |
| [23] | B. H. Liskov, J. M. Wing, A behavioral notion of subtyping, ACM Trans. Programming Languages Systems.; B. H. Liskov, J. M. Wing, A behavioral notion of subtyping, ACM Trans. Programming Languages Systems. |
| [24] | Lynch, N.; Vaandrager, F., Forward and backward simulations—Part Iuntimed systems, Inform. and Comput., 121, 2, 214-233 (1995), also: Technical Memo MIT \(/\) LCS \(/\) TM-486.b, Laboratory for Computer Science, MIT · Zbl 0834.68123 |
| [25] | R. Miarka, E. Boiten, J. Derrick, Guards, preconditions, and refinement in Z, in: J. Bowen, S. Dunne, A. Galloway, S. King (Eds.), ZB2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 1878, Springer, Berlin, 2000, pp. 286-303.; R. Miarka, E. Boiten, J. Derrick, Guards, preconditions, and refinement in Z, in: J. Bowen, S. Dunne, A. Galloway, S. King (Eds.), ZB2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, Vol. 1878, Springer, Berlin, 2000, pp. 286-303. |
| [26] | J. Moore, PITON: a verified assembly level language, Technical Report 22, Computational Logic Inc., available at the URL:; J. Moore, PITON: a verified assembly level language, Technical Report 22, Computational Logic Inc., available at the URL: |
| [27] | Reif, W.; Schellhorn, G.; Stenzel, K.; Balser, M., Structured specifications and interactive proofs with KIV, (Bibel, W.; Schmitt, P., Automated Deduction—A Basis for Applications (1998), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 13-39 · Zbl 0970.68149 |
| [28] | G. Schellhorn, Verification of Abstract state machines, Ph.D. thesis, Universität Ulm, Fakultät für Informatik, (available at; G. Schellhorn, Verification of Abstract state machines, Ph.D. thesis, Universität Ulm, Fakultät für Informatik, (available at |
| [29] | Schellhorn, G., Verification of ASM refinements using generalized forward simulation, J. Universal Comput. Sci. (J.UCS), 7, 11, 952-979 (2001), available at |
| [30] | Schellhorn, G.; Ahrendt, W., The WAM case studyverifying compiler correctness for prolog with KIV, (Bibel, W.; Schmitt, P., Automated Deduction—A Basis for Applications (1998), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 165-194 · Zbl 0977.68017 |
| [31] | J.M. Spivey, The Z Notation: A Reference Manual, second ed., International Series in Computer Science, Prentice-Hall, Englewood Cliffs, NJ, 1992.; J.M. Spivey, The Z Notation: A Reference Manual, second ed., International Series in Computer Science, Prentice-Hall, Englewood Cliffs, NJ, 1992. · Zbl 0777.68003 |
| [32] | R.F. Stärk, S. Nanchen, A complete logic for abstract state machines, J. Universal Comput. Sci. (J.UCS) Abstract State Machines 2001: Theory and Applications 7 (11) (2001) 981-1006.; R.F. Stärk, S. Nanchen, A complete logic for abstract state machines, J. Universal Comput. Sci. (J.UCS) Abstract State Machines 2001: Theory and Applications 7 (11) (2001) 981-1006. |
| [33] | J.C.P. Woodcock, J. Davies, Using Z: Specification, Proof and Refinement, Prentice-Hall International Series in Computer Science, 1996.; J.C.P. Woodcock, J. Davies, Using Z: Specification, Proof and Refinement, Prentice-Hall International Series in Computer Science, 1996. · Zbl 0855.68060 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
