Advertisement

Composing Event Constraints in State-Based Specification

  • Tommaso Bolognesi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)

Abstract

Event-based process algebraic specification languages support an elegant specification technique by which system behaviours are described as compositions of constraints on event occurrences and event parameters. This paper investigates the possibility to export this specification paradigm to a state-based formalism, and discusses some deriving advantages in terms of verification.

Keywords

Formal Method Parallel Operator Process Algebra Active Port Abstract State Machine 
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.

References

  1. 1.
    Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  2. 2.
    Woodcock, J.C.P., Cavalcanti, A.L.C.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Gurevich, Y.: Evolving Algebras 1993 - Lipari Guide. In: Boerger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford Univ. Press, Oxford (1995)Google Scholar
  4. 4.
    Boerger, E., Staerk, R.: Abstract State Machines - A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Abrial, J.R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  6. 6.
    Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16, 872–923 (1994)CrossRefGoogle Scholar
  7. 7.
    Lamport, L.: Specifying Systems - The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2003)Google Scholar
  8. 8.
    Spivey, J.M.: The Z Notation - A Reference manual. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  9. 9.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  10. 10.
    Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)CrossRefzbMATHGoogle Scholar
  11. 11.
    Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems 14, 25–59 (1987)CrossRefGoogle Scholar
  12. 12.
    Brinksma, E.: ISO, Information Processing Systems, Open Systems Interconnection, LOTOS, a formal description technique based on the temporal ordering of observational behaviour - IS8807. Technical report, Geneva (1989)Google Scholar
  13. 13.
    Quemada, J., Azcorra, A.: A constraint oriented specification of al’s node. In: van Eijk, P.H.J., Vissers, C.A., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 83–88. North-Holland, Amsterdam (1989)Google Scholar
  14. 14.
    Bolognesi, T.: Deriving graphical representations of process networks from algebraic expressions. Information Processing Letters 46, 289–294 (1993)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Tommaso Bolognesi
    • 1
  1. 1.CNR – ISTIItaly

Personalised recommendations