The formal semantics of a domain-specific modelling language

Thesis

Abstract:: The Specification and Description Language (SDL) was developed by the telecommunications industry as a common language for the design of asynchronous communicating systems. Designs expressed in SDL can be given a formal, mathematical interpretation to facilitate analysis and to guide correct implementation. The standard formalisation of SDL is adequate for the purposes of language definition, but is not oriented towards either analysis or implementation of specific designs. This thesis investigates alternative approaches to the formalisation of SDL. A specific, constrained version of the language is considered: one more amenable to code generation. A statebased formalisation is presented using the Z notation, together with a process-based account using the language of Communicating Sequential Processes. A more abstract, elegant solution is then proposed, in terms of a calculus of buffered systems, itself given an interpretation using Hoare and He's Unifying Theories of Programming. A case study is presented to demonstrate the practical application of the formalisations.

Language:: English
Keywords:: specification

Ericsson

language

Java

SDL

description

CSP

UML

PLEX

telecomunications

Z
Subjects:: Program development and tools

Computer science (mathematics)

Communication Sequential Processing (CSP)

Theory and automated verification

Software engineering
UUID:: uuid:79a08914-9ab2-4085-9fa7-a2662059e32a
Local pid:: ora:4615
Deposit date:: 2010-12-14
ARK identifier:: ark:/29072/ora_79a089149ab240859fa7a2662059e32a

Licence:: Terms and Conditions of Use for Oxford University Research Archive

If you are the owner of this record, you can report an update to it here: Report update to this record