The formal semantics of a domain-specific modelling language

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