@inproceedings{612d87c19dc34f14839f68305eb94b30,
title = "Specification of required non-determinism",
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.",
keywords = "Temporal Logic, Parallel Composition, Composite Action, Action Symbol, Linear Time Temporal Logic",
author = "K. Lano and J. Bicarregui and J. Fiadeiro and A. Lopes",
year = "1997",
doi = "10.1007/3-540-63533-5\_16",
language = "English",
isbn = "3540635335",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "298--317",
editor = "J. Fitzgerald and Jones, \{C. B.\} and P. Lucas",
booktitle = "FME 1997",
address = "Germany",
note = "4th International Symposium of Formal Methods Europe, FME 1997 ; Conference date: 15-09-1997 Through 19-09-1997",
}