Verification of SDL Specifications on the Basis of Stream Semantics

This paper presents a new approach to the formal verification of SDL specifications. SDL is given denotational semantics based on the concepts of streams and stream processing functions in the formal framework of Focus. The formalization of SDL revealed some aspects of SDL which are handled unprecisely in the Z.100, e.g., the concept of time, and gives a solution to them. The formal semantics is the starting point for a verification method for SDL specifications. Properties of SDL specifications can now be proved in the mathematical, logical framework of domain theory. To document the use of the verification method, we outline the results of a case study in which we proved the correctness of the SDL specification of the well-known alternating bit protocol. Keywords SDL, semantics, streams, stream processing functions, verification, time, Focus 1. INTRODUCTION Formal verification allows to mathematically prove that a specification fulfils desired properties. As a prerequisite, forma..