Specification of required non-determinism

  • K. Lano
  • J. Bicarregui
  • J. Fiadeiro
  • A. Lopes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


We present an approach to the specification of required external non-determinism: the willingness of a component to respond to a number of external action requests, using a language, COMMUNITY, which provides both permission and willingness guards on actions.

This enables a program-like declaration of required non-determinism, in contrast to the use of a branching-time temporal logic. We give a definition of parallel composition for this language, and show that refinement is compositional with respect to parallel composition. We use the concepts developed for COMMUNITY to identify extensions to the B and VDM++ model-based specification languages to incorporate specification of required non-determinism. In particular, we show that preconditions may be considered as a form of willingness guard, separating concerns of acceptance and termination, once module contracts are re-interpreted in a way suitable for a concurrent environment.


Temporal Logic Parallel Composition Composite Action Action Symbol Linear Time Temporal Logic 
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.
    J-R Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  2. 2.
    J-R Abrial. Extending B Without Changing it (for Developing Distributed Systems), B Conference, IRIN, Nantes, November 1996.Google Scholar
  3. 3.
    M Butler. Stepwise Refinement of Communicating Systems, Southampton University, 1997.Google Scholar
  4. 4.
    K M Chandy and J Misra. Parallel Program Design-A Foundation. AddisonWesley, 1988.Google Scholar
  5. 5.
    S Cook and J Daniels. Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice Hall, Sept 1994.Google Scholar
  6. 6.
    J Fiadeiro and T Maibaum. Temporal Theories as Modularisation Units for Concurrent System Specification, Formal Aspects of Computing 4(3), pp. 239–272, 1992.CrossRefGoogle Scholar
  7. 7.
    J Fiadeiro and T Maibaum. Categorical Semantics of Parallel Program Design, Science of Computer Programming, 28 (1997), pp. 111–138, 1997.Google Scholar
  8. 8.
    C B Jones. Accommodating Interference in the formal design of concurrent objectbased programs. Formal Methods in System Design, 8(2): 105–122, March 1996.Google Scholar
  9. 9.
    R Kuiper. Enforcing Nondeterminism via Linear Time Temporal Logic Specification using Hiding, in B Banieqbal, H Barringer and A Pnueli (eds) Temporal Logic in Specification, LNCS 398, Springer-Verlag 1989, 295–303.Google Scholar
  10. 10.
    K Lano, S Goldsack, J Bicarregui and S Kent. Integrating VDM ++ and Real-Time System Design, Z User Meeting, 1997.Google Scholar
  11. 11.
    A Lopes. COMMUNITY and Required Non-determinism, Department of Informatics, University of Lisbon, 1996.Google Scholar
  12. 12.
    C McHale. Synchronisation in Concurrent, Object-oriented Languages: Expressive Power, Genericity and Inheritance. PhD Thesis, University of Dublin, 1995.Google Scholar
  13. 13.
    C Stirling. Comparing linear and branching time temporal logics. In B Baniegbal, H Barringer and A Pnueli (eds) Temporal Logic in Specification, LNCS 398, Springer-Verlag 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • K. Lano
    • 1
  • J. Bicarregui
    • 1
  • J. Fiadeiro
    • 2
  • A. Lopes
    • 2
  1. 1.Dept. of ComputingImperial CollegeLondon
  2. 2.Dept. of InformaticsUniversity of LisbonCampo Grande

Personalised recommendations