Abstract
A specification language for nonsequential systems that unifies algebraic specifications of abstract data types with high-level Petri net specifications of dynamic behavior is presented. The data structure of a system, the information content of local states, and static constraints to state changing operations are specified by sorted Horn clause rules with equality. Behavior is specified by schemes of Predicate-Event nets together with an initial (distributed) state. Many-sorted algebras provide a standard interpretation of such specifications in terms of the initial models satisfying the rules, the flow, and the initial state given. One concern of this paper is to sketch the mathematical semantics of the core language. The other is to define a notion of abstract system that supports modularity and reusability of specifications similar to abstract data types.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Berthomieu, N. Choquet, C. Colin, B. Loyer, J. Martin, and A. Mauboussin. Abstract data nets combining Petri nets and abstract data types for high level specifications of distributed systems. In Proceedings of the 7th European Workshop on Applications and Theory of Petri Nets, pages 25–48, Oxford, England, July 1986.
E. Best and C. Fernàndez. Notations and terminology on Petri net theory. Petri Net Newsletter, 23: 21–46, April 1986.
M. Broy and M. Wirsing. Partial abstract types. Acta Informatica, 18: 47–64, 1982.
M. Diaz. Modelling and analysis of communication and cooperation protocols using Petri net based models. In C. A. Sunshine, editor, Protocol Specification, Testing and Verification, pages 465–510, North-Holland Publishing Company, 1982.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Volume 6 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.
K. Futatsugi, J. A. Goguen, J. Jouannaud, and J. Meseguer. Principles of OBJ2. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 5266, Louisiana, New Orleans, 1985.
H. J. Genrich and K. Lautenbach. System modelling with high-level Petri nets. Theoretical Computer Science, 13 (1): 109–136, 1981.
S. L. Gerhart, D. Musser, D. Thompson, D. Baker, R. Bates, R. Erickson, R. London, D. Taylor, and D. S. While. An overview of Affirm: a specification and verification system. In S. Lavington, editor, INFORMATION PROCESSING 80, pages 343–347, IFIP, North-Holland Publishing Company, 1980.
J. A. Goguen and J. Meseguer. EQLOG: equality, types and generic modules for logic programming. In D. DeGroot and G. Lindstrom, editors, Functional and Logic Programming, pages 295–363, Prentice-Hall, 1986.
J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, pages 80–149, Prentice-Hall, Englewood Cliffs, New Jersey, 1978.
B. Krämer. MYNAS - a formal language combining Petri nets and Abstract Data Types for specifying distributed systems. In Proceedings of the 9th Annual International Conference on Software Engineering, pages 116–125, Monterey, California, March 1987.
B. Krämer. S82RAS - The GRASPIN Specification Language. GRASPIN Technical Paper, Sankt Augustin, July 1986.
B. Krämer. Stepwise construction of non-sequential software systems using a net based specification language. In G. Rozenberg, editor, Advances in Petri nets 1984, pages 307–327, Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.
B. Krämer and H. Schmidt. An approach to algebraic specification and stepwise implementation of non-sequential systems. In Poster Session Proceedings of the 6th International Conference on Software Engineering, pages 63–64, Information Processing Society of Japan, Tokyo, Japan, September 1982.
H. Kreowski and H. Schmidt. Some Algebraic Concepts of the Specification Language SCOW and their Initial Semantics. GMD-Studien, Gesellschaft für Mathematik und Datenverarbeitung, October 1984.
L. Lamport. On interprocess communication, part I. Distributed Computing, 1: 77–85, 1986.
L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages, 5 (2): 190–222, April 1983.
B. Mahr and J. Makowsky. Characterizing specification languages which admit initial semantics. Theoretical Computer Science, 31: 49–60, 1984.
R. A. Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Springer-Verlag, Berlin, Heidelberg, New York, 1980.
B. Möller. Algebraic specification with higher-order operators. In L. Meertens, editor, Proceedings of the IFIP TC 2 Working Conference on Program Specification and Transformation North-Holland, Amsterdam, to appear
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science pages 46–57, Providence, October 1986.
A. Poigné. On specifications, theories, and models with higher types. Information and Control, 68(1–3), January, February, March 1986.
W. Reisig. Petri Nets. Volume 4 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.
H. Schmidt. Towards a Net-Theoretic Notion of Type based on Predicate-Transition Nets. Arbeitspapiere der GMD 117, Gesellschaft für Mathematik und Datenverarbeitung, November 1984.
H. Schmidt and M. Papazoglou. Abstract Implementation of Predicate-Event Systems. Sankt Augustin, August 1985.
J. Vautherin. Parallel systems specifications with colored Petri nets and algebraic abstract data types. In Proceedings of the 7th European Workshop on Applications and Theory of Petri Nets, pages 5–23, Oxford, England, July 1986.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Krämer, B., Schmidt, H.W. (1991). Types and Modules for Net Specifications. In: Jensen, K., Rozenberg, G. (eds) High-level Petri Nets. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-84524-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-84524-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54125-7
Online ISBN: 978-3-642-84524-6
eBook Packages: Springer Book Archive