Specification of required non-determinism

K. Lano, J. Bicarregui, J. Fiadeiro, A. Lopes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationFME 1997
Subtitle of host publicationIndustrial Applications and Strengthened Foundations of Formal Methods - 4th International Symposium of Formal Methods Europe, Proceedings
EditorsJ. Fitzgerald, C. B. Jones, P. Lucas
Place of PublicationBerlin
PublisherSpringer Verlag
Number of pages20
ISBN (Electronic)9783540695936
ISBN (Print)3540635335, 9783540635338
Publication statusPublished - 1997
Event4th International Symposium of Formal Methods Europe, FME 1997 - Graz, Austria
Duration: 15 Sept 199719 Sept 1997

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference4th International Symposium of Formal Methods Europe, FME 1997


  • Temporal Logic
  • Parallel Composition
  • Composite Action
  • Action Symbol
  • Linear Time Temporal Logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Specification of required non-determinism'. Together they form a unique fingerprint.

Cite this