Specification of required non-determinism
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.
KeywordsTemporal Logic Parallel Composition Composite Action Action Symbol Linear Time Temporal Logic
Unable to display preview. Download preview PDF.
- 1.J-R Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
- 2.J-R Abrial. Extending B Without Changing it (for Developing Distributed Systems), B Conference, IRIN, Nantes, November 1996.Google Scholar
- 3.M Butler. Stepwise Refinement of Communicating Systems, Southampton University, 1997.Google Scholar
- 4.K M Chandy and J Misra. Parallel Program Design-A Foundation. AddisonWesley, 1988.Google Scholar
- 5.S Cook and J Daniels. Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice Hall, Sept 1994.Google Scholar
- 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.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.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.K Lano, S Goldsack, J Bicarregui and S Kent. Integrating VDM ++ and Real-Time System Design, Z User Meeting, 1997.Google Scholar
- 11.A Lopes. COMMUNITY and Required Non-determinism, Department of Informatics, University of Lisbon, 1996.Google Scholar
- 12.C McHale. Synchronisation in Concurrent, Object-oriented Languages: Expressive Power, Genericity and Inheritance. PhD Thesis, University of Dublin, 1995.Google Scholar
- 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