Editor's Note:
This is an abstract of a recent thesis. The thesis is available as
Computing Science Technical Report CSM-120 from the University of Stirling
at a cost of 
5. Please contact Mrs. Moira Taylor
(moira.taylor@compsci.stirling.ac.uk) if you would like to obtain a copy.
This thesis uses the language (ISO International Standard ISO 8807)
as a basis for the formal specification of distributed systems.
Contributions are made to two key research areas: architecture-driven
specification and 
language extensions.
The notion of architecture-driven specification is to guide the
specification process by providing a reference-base of pre-defined
domain-specific components. The thesis builds an infra-structure of
architectural elements, and provides Extended (XL)
definitions of these elements.
The thesis develops Extended (XL) for the specification of
distributed systems. XL is enhanced with features for the formal
specification of quantitative timing, probabilistic and priority
requirements. For distributed systems, the specification of these
`performance' requirements can be as important as the specification of the
associated functional requirements.
To support quantitative timing features, the XL semantics define a global, discrete clock which can be used both to force events to occur at specific times, and to measure intervals between event occurrences. XL introduces time-policy operators ASAP (`as soon as possible' corresponding to `maximal progress semantics') and ALAP (`as late as possible'). Special internal transitions are introduced in XL semantics for the specification of probability. Conformance relations based on a notion of probabilisation, together with a testing framework, are defined to support reasoning about probabilistic XL specifications. Priority within the XL semantics ensures that permitted events with the highest priority weighting of their class are allowed first.
Both functional and performance specification play important rôles in CIM (Computer Integrated Manufacturing) systems. The thesis uses a CIM system known as the CIM-OSA Integrating Infrastructure as a case-study of architecture-driven specification using XL.
The thesis thus constitutes a step in the evolution of distributed system specification methods that have both an architectural basis and a formal basis.