ePubs
The open archive for STFC research publications
Home
About ePubs
Content Policies
News
Help
Privacy/Cookies
Suggest an Enhancement
Contact ePubs
Full Record Details
Persistent URL
http://purl.org/net/epubs/work/25594
Record Status
Checked
Record Id
25594
Title
A Model Oriented Analysis of a Communications Protocol
Contributors
Juan C Bicarregui (SERC Rutherford Appleton Lab.)
Abstract
In [BA92], Bruns and Anderson describe a communications protocol in CCS with value-passing. A data model of the state is given in terms of the type constructors usually found in model-oriented specification. For the agents described, a series of semaphores ensure exclusive access to the state, thus the behaviour can be described as a purely sequential system. This paper considers some alternative data-models for this system: two abstractions and two reifications of the original specification are given. In particular, strong invariants are used to exclude unreachable values from the state space. The example raises some stylistic questions concerning how much detail, that can be inferred from the invariant, should be left implicit in postconditions. VDM is used for the development, and the role of the explicit frames of reference in the operation definitions is examined in some detail. The interaction between read and write frames and invariant is studied, as is the manner by which the information in the frames is propagated during refinement. Also examined, is how the use of these frames can be extended and how their use can be combined with operation structuring mechanisms available in other model-oriented methods. The paper concludes with a discussion of some general questions of methodology raised by the example.
Organisation
SERC
Keywords
Funding Information
Related Research Object(s):
Licence Information:
Language
English (EN)
Type
Details
URI(s)
Local file(s)
Year
Report
RAL Technical Reports
RAL-93-099. 1993.
RAL-TR-1993-099.pdf
1993
Showing record 1 of 1
Recent Additions
Browse Organisations
Browse Journals/Series
Login to add & manage publications and access information for OA publishing
Username:
Password:
Useful Links
Chadwick & RAL Libraries
SHERPA FACT
SHERPA RoMEO
SHERPA JULIET
Journal Checker Tool
Google Scholar