Abstract
The object-oriented specification of concurrent and distributed systems has tended to emphasise the aspect of substitutability at the expense of code reuse. A variety of constraints has been imposed in order to guarantee substitutability in one form or another. This paper argues that the incremental development of software specifications needs to consider substitutability in the context of code reuse. Further, the common approach of starting with an abstract specification and then progressively refining it (in some general way) means that many existing substitutability constraints are too strong. In the context of Coloured Petri Nets, we advocate the use of three specific forms of refinement — type refinement, subnet refinement, and node refinement. These have weaker demands for substitutability, namely that every (complete) refined behaviour has a corresponding abstract behaviour, but not necessarily vice versa. An examination of case studies in the literature suggests that this approach is applicable in practice.
Chapter PDF
Similar content being viewed by others
References
W.M.P. van der Aalst and T. Basten. Life-cycle Inheritance: A Petri-NetBased Approach. In P. Azema and G. Balbo, editors, Application and Theory of Petri Nets 1997, volume 1248 of Lecture Notes in Computer Science, pages 62–81, Tolouse, France, 1997. Springer-Verlag.
C. Balzarotti, F. DeCindio, and L. Pomello. Observation Equivalences for the Semantics of Inheritance. In IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems,Florence, Italy, February 15–18, 1999. Chapman and Hall.
B. Baumgarten. Petri-Netze: Grundlagen und Anwendungen. Mannheim: BI-Wissenschaftsverlag, 1990.
H. Bowman, C. Briscoe-Smith, J. Derrick, and B Strulo. On Behavioural Subtyping in LOTOS. In Second IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems. Chapman and Hall, 1997.
L. Cardelli and J. C. Mitchell. Operations on Records. In D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné, editors, Proceedings of the Conference on Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 75–81, Berlin, September 1989. Springer.
A. Diller. Z: An Introduction to Formal Methods. John Wiley & Sons, 2nd edition, 1994.
D. J. Floreani, J. Billington, and A. Dadej. Designing and Verifying a Communications Gateway Using Coloured Petri Nets and Design/CPN. Lecture Notes in Computer Science, 1091: 153–171, 1996.
D.J. Floreani. The Interconnection of Tactical Packet Radio Networks and BISDN. PhD thesis, School of Physics and Electronic Systems Engineering, University of South Australia, 1996.
A. Goldberg and D. Robson. Smalltalk-80: The Language and its Implementation. Addison-Wesley, 1983.
K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use: Volume 1, Analysis Methods. Monographs in Theoretical Computer Science. Springer-Verlag, Berlin, Germany, 1992.
K. Jensen, S. Christensen, P. Huber, and M. Holla. Design/CPN TM : A Reference Manual. MetaSoftware Corporation, 1992.
C. Lakos. On the Abstraction of Coloured Petri Nets. In P. Azéma and G. Balbo, editors, Lecture Notes in Computer Science: 18th International Conference on Application and Theory of Petri Nets, Toulouse, France, June 1997, volume 1248, pages 42–61. Springer-Verlag, June 1997.
C. Lakos. Composing Abstractions of Coloured Petri Nets. In Proceedings of the 21st International Conference on Applications and Theory of Petri Nets (to apppear), Aarhus, Denmark, June 2000.
C. Lakos and J. Lamp. The Incremental Modelling of the Z39.50 Protocol with Object Petri Nets. Lecture Notes in Computer Science, 1605: 37–68, 1999.
C. Lakos and G. Lewis. A Catalogue of Incremental Changes for Coloured Petri Nets. Technical report TR99–02, Department of Computer Science, University of Adelaide, 1999.
W. LaLonde and J. Pugh. Subclassing 0 Subtyping 0 Is-a. Journal of Object-Oriented Programming, pages 57–60, January 1991.
G. Lewis and C. Lakos. Incremental Reachability Algorithms. Technical report TR99–01, Department of Electrical Engineering and Computer Science, University of Tasmania, 1999.
B Meyer. Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs, first edition, 1988.
A. B. Mnaouer, T. Sekiguchi, Y. Fujii, and T. Ito. Coloured Petri Nets Based Modelling and Simulation of the Static and Dynamic Allocation Policies of the Asynchronous Bandwidth in the Fieldbus Protocol. Lecture Notes in Computer Science, 1605: 93–130, 1999.
O. Nierstrasz. Regular Types for Active Objects. ACM Sigplan Notices, 28 (10): 1–15, October 1993. Proceedings of the 8th. annual conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA’93, Washington DC, 1993.
W. Reisig. Petri Nets in Software Engineering. Lecture Notes in Computer Science, 255: 63–96, 1987.
P. Wegner and S. B. Zdonik. Inheritance as an Incremental Modification Mechanism or What Like Is and Isn’t Like. Lecture Notes in Computer Science, 322: 55–77, 1988.
Glynn Winskel. Petri Nets, Algebras, Morphisms, and Compositionality Information and Computation, 72 (3): 197–238, March 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this paper
Cite this paper
Lakos, C., Lewis, G. (2000). A Practical Approach to Incremental Specification. In: Smith, S.F., Talcott, C.L. (eds) Formal Methods for Open Object-Based Distributed Systems IV. FMOODS 2000. IFIP Advances in Information and Communication Technology, vol 49. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35520-7_12
Download citation
DOI: https://doi.org/10.1007/978-0-387-35520-7_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-1018-2
Online ISBN: 978-0-387-35520-7
eBook Packages: Springer Book Archive