The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/28919
Record Status Checked
Record Id 28919
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.
Organisation CCLRC , BITD
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings In Fourth International Sumposium of Formal Methods Europe (FME'97), Graz, Austria, September 15-19, 1997, (1997). FME97.pdf 1997