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)

Abstract

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
Pages298-317
Number of pages20
ISBN (Electronic)9783540695936
ISBN (Print)3540635335, 9783540635338
DOIs
Publication statusPublished - 1997
Event4th International Symposium of Formal Methods Europe, FME 1997 - Graz, Austria
Duration: 15 Sep 199719 Sep 1997

Publication series

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

Conference

Conference4th International Symposium of Formal Methods Europe, FME 1997
CountryAustria
CityGraz
Period15/09/9719/09/97

Keywords

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

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

  • Cite this

    Lano, K., Bicarregui, J., Fiadeiro, J., & Lopes, A. (1997). Specification of required non-determinism. In J. Fitzgerald, C. B. Jones, & P. Lucas (Eds.), FME 1997: Industrial Applications and Strengthened Foundations of Formal Methods - 4th International Symposium of Formal Methods Europe, Proceedings (pp. 298-317). (Lecture Notes in Computer Science; Vol. 1313). Springer Verlag. https://doi.org/10.1007/3-540-63533-5_16