OBJSA Nets: OBJ and Petri Nets for Specifying Concurrent Systems

  • E. Battiston
  • F. De Cindio
  • G. Mauri
Part of the Advances in Formal Methods book series (ADFM, volume 2)


This paper provides an intuitive presentation of OBJSA nets, a specification language which combines a specific class of Petri nets, namely Superposed Automata nets, and the well-known algebraic specification language OBJ. The presentation is particularly addressed to people confident with algebraic specification techniques and focuses on the composition mechanism which allows the designer to obtain the OBJSA specification of a system by combining the specifications of the system components.


Software Engineering Elementary Component Input Place Output Place Incremental Development 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E. Astesiano, G. Reggio. Algebraic Specification of Concurrency, in:Recent Trends in Data Type Specification, LNCS 655, (M. Bidoit, C. Choppy), pp. 1–39, Springer Verlag, 1993.Google Scholar
  2. [2]
    E. Battiston, O. Botti, E. Crivelli, F. De Cindio. An Incremental Specification of a Hydroelectric Power Plant Control System using a class of modular algebraic nets, in: Proc. of the “16th Int. Conference on Application and Theory of Petri nets, Torino, I, 28à30 June 1995”, LNCS 935, (G. De Michelis, M. Diaz), pp. 84–102, Springer Verlag,1995.Google Scholar
  3. [3]
    E. Battiston, V. Crespi, F. De Cindio, G. Mauri. Semantics frameworks for a class of modular algebraic nets, inProc. of the “3rd Int. Conference on Algebraic Methodology and Software Technology, AMAST ‘83, Enschede, NL, 21–25 June 1993”, Workshops in Computing, (M. Nivat, C.Rattay, T.Rus and G.Scollo), pp. 271–280, Springer-Verlag, 1993.Google Scholar
  4. [4]
    E. Battiston, F. De Cindio, G. Mauri. OBJSA nets: a class of high level nets having objects as domains, in “Advances in Petri Nets 88”, LNCS 340, (G. Rozenberg ed.), pp. 20–43, Springer Verlag,1988. Also in [20].Google Scholar
  5. [5]
    E. Battiston, F. De Cindio, G. Mauri, L. Rapanotti. Morphisms and Minimal Models for OBJSA Nets, in Proc. of the “12th Int. Conference on Application and Theory of Petri nets, Gjern, DK, 26à28 June 1991”, pp. 455–476.Google Scholar
  6. [6]
    L. Bernardinello, F. De Cindio. A survey of basic net models and modular net classes. inAdvances in Petri Nets 1992, LNCS 609, (G.Rozenberg ed.), pp. 304–351, Springer Verlag, 1992.Google Scholar
  7. [7]
    E.Best. DEMON (Design Methods Based on Nets): Aims, Scope and Achievements. inAdvances in Petri Nets 1992, LNCS 609, (G.Rozenberg ed.), pp. 1–20, Springer Verlag, 1992.Google Scholar
  8. [8]
    D. Bouchs, N. Guelfi. CO-OPN: A Concurrent Object Oriented Petri Net Approach. in Proc. of the “12th Int. Conference on Application and Theory of Petri nets, Gjern, DK, 26à28 June 1991”, pp. 432–454.Google Scholar
  9. [9]
    A. Bouali, S. Gnesi, S. Larosa. The Integration Project for the JACK Environment. in Bulletin of EATCS, 54, pp. 207–223, October 1994.Google Scholar
  10. [10]
    F.De Cindio, G. De Michelis, L. Pomello, C. Simone. Superposed Automata Nets. in “Application and Theory of Petri Nets”, 11413 52, (C. Girault and W. Reisig), pp. 269–279, Springer Verlag, 1982.Google Scholar
  11. [11]
    R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. in Computer Network and ISDN systems, 25, 7, pp. 761–778, North Holland, 1993.Google Scholar
  12. [12]
    F.De Cindio, G.A. Lanzarone, A. Torgano. An SA Net Model of SDL. in Proc. of “5th European Workshop on Applications and Theory of Petri Nets, Aarhus, DK,1984”.Google Scholar
  13. [13]
    R. De Nicola and U.Montanari (eds.). Selected Papers of “Second Workshop on Concurrency and Compositionality, San Miniato, I, March 1990”, TCS 96, 1, 1992.Google Scholar
  14. [14]
    H. Ehrig, B. Mahr. Fundamentals of algebraic specification 1. Springer-Verlag, Berlin, 1985.CrossRefGoogle Scholar
  15. [15]
    H. Genrich. Predicate/Transition nets. in “Advances in Petri Nets 86, Part I”, LNCS 254, (W. Brauer, W. Reisig, G. Rozenberg), pp. 207–247, Springer-Verlag, 1987.Google Scholar
  16. [16]
    J.A. Goguen, J.W. Thatcher, E.G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. in “Current Trends in Programming Methodology IV: Data structuring”, (R. Yeh, Ed.), pp. 80–144, Prentice Hall, 1978.Google Scholar
  17. [17]
    J.A. Goguen, T. Winkler. Introducing OBJ3. Report SRI-CSL-88–9, August 1988.Google Scholar
  18. [18]
    C.A.R. Hoare. Communicating sequential processes. in CACM, 21, pp. 666–677, 1978.Google Scholar
  19. [19]
    K. Jensen. Coloured Petri nets. in “Advances in Petri Nets 90”, LNCS 483, (G. Rozenberg ed), pp. 342–416, Springer Verlag, 1990. Also in [20].Google Scholar
  20. [20]
    K. Jensen and G. Rozenberg (eds). High–level Petri Nets. Theory and Application. ISBN: 3–540–54125 X or 0–387–54125 X, Springer Verlag,1991.Google Scholar
  21. [21]
    K.P.Lohr. Concurrency annotations for reusable software. in CACM, 36, 9, pp. 81–89, 1993.Google Scholar
  22. [22]
    P.E. Lauer, P.R. Torrigiani, M.W. Shields. COSY- A System Specification Language Based on Paths and Processes. in Acta Informatica, 12, pp.109158, 1979.Google Scholar
  23. [23]
    B. Liskov, S. Zilles. An introduction to Formal Specifications of Data Abstractions. in “Current Trends in Programming Methodology I: Software Specification and Design”, (R. Yeh ed.), pp. 1–32, Prentice-Hall, 1978.Google Scholar
  24. [24]
    J. Malhotra. DesignML. Reference Manual. Meta Software Co., Cambridge, MA, USA,1990.Google Scholar
  25. [25]
    J. Meseguer. Rewriting as a unified model of concurrency. in [13], 1992.Google Scholar
  26. [26]
    B. Meyer. Sequential and Concurrent Object-Oriented Programming. in CACM, 36, 9, pp. 56–80, 1993.Google Scholar
  27. [27]
    R. Milner. A calculus for communicating systems. LNCS 92, Springer Verlag,1980.Google Scholar
  28. [28]
    J. Meseguer, U. Montanari. Petri nets are monoids. in Information and Computation, 88, 2, 1990.Google Scholar
  29. [29]
    W. Reisig. Petri Nets with Algebraic Specifications. in TCS, 80, pp. 1–34, 1991. Also in [20].Google Scholar
  30. [30]
    W. Reisig, E. Smith. The semantics of a net is a net. An exercise in general net theory. in “Concurrency and Nets”, (K. Voss, H. Genrich, G. Rozenberg), pp. 269–286, Springer Verlag, 1987.Google Scholar
  31. [31]
    T. Winkler. Introducing OBJ3’s New Features. Report SRI-CSL, 1992.Google Scholar
  32. [32]
    S.N. Zilles. Algebraic specification of data types. Project MAC Progress Report 11, pp. 28–52, MIT, Cambridge, Mass., 1974.Google Scholar

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • E. Battiston
    • 1
  • F. De Cindio
    • 1
  • G. Mauri
    • 1
  1. 1.Dipartimento di Science dell’InformazioneUniversitá di MilanoMilanoItaly

Personalised recommendations