Define a formal semantics for TTCN (Tree and Tabular Combined Notation)

Denotational method is a powerful formalism for semantic specifications of programming languages. It has been successfully applied to some real world sequential programming languages. However, few efforts have ever been made successfully toward using it to specify semantics for concurrent and parallel programming languages because of the difficulties of describing communicating processes, which are usually specified by some other formal models such as the communicating finite state machine and process algebra.; This dissertation first proposes a generic denotational semantic model {dollar}(Phi, muPhi){dollar} for communicating processes, where {dollar}Phi{dollar} is a continuous function and {dollar}muPhi{dollar} is the least fixed point of {dollar}Phi.{dollar} This formal model attempts to be concise, intuitive, direct, consistent and able to describe all the static and dynamic, finite and infinite aspects of communicating processes including time processes and timer operations. Therefore the semantic specification issues for concurrent and parallel programming languages can also be resolved in the same way as for the sequential programming languages.; As part of International Standard IS 9646, TTCN (Tree and Tabular Combined Notation) is a notation for specification of abstract test suites of OSI (Open System Interconnection) protocol conformance testing. As a concurrent/parallel programming language, TTCN has no formally specified language semantics yet, though it has formally specified syntax and clearly but not formally specified operational semantics. This is a drawback for IS 9646 and an obstacle to the efforts of automatically deriving executable test suites from abstract test suites through compiler/translator techniques.; This dissertation then contributes a formal semantic specification for the TTCN language based on the proposed denotational semantic model for communicating processes and other denotational techniques. The formal specification of TTCN semantics is given in such a way that both the static and dynamic semantics are specified with an unique mathematical notation of an extended {dollar}lambda{dollar}-calculus.