Concepts, Syntax and Semantics of SEGRAS. A Specification Language for Distributed Systems

摘要

The thesis presents SEGRAS, a new language for writing, testing, and analyzing formal specifications of nonsequential and distributed software systems. The language treats data abstractions with states and state-dependent operations that can dynamically create new data objects and concurrently modify their properties according to a specified nonsequential behavior. In the first part of the thesis the kernel concepts of the SEGRAS language are presented and a denotational semantics is given for them. Many-sorted partial algebras provide a semantics of data specifications, and Condition-Event systems provide a net semantics of nonsequential behavior. To increase the practical value of the language, its type system is extended in Part II by parametric types and a restricted form of function types and dependent types. The additional expressive power of the extended type system is demonstrated through a series of examples. Its semantics is defined in terms of a logical deduction system. As a practical solution to the problem of determining the well-typing of SEGRAS specifications, a sound compile time type checking algorithm is presented.