Browse Theses

Formal specifications play a central role in developing large, complex and reliable software systems. Object-oriented programming, an accepted and proven technology of the recent years, provides important benefits for software development to the software industry. An object-oriented specification is a formal description of the object-oriented decomposition, abstraction, and design of a system of interest. However, various fundamental issues in formal specifications for object-oriented systems remain largely unexplored. Hence, the current research is focused on both the theoretical and practical aspects of object-oriented specifications.

The purpose of this dissertation is to develop a specification language for object-oriented systems and a set of formal methods for constructing disciplined specifications. Hence, we develop a model-oriented specification language TOSS for writing formal specifications of object-oriented systems. The main design principle of the language is to provide a high degree of flexibility and expressiveness without unduly compromising security and formality, where flexibility and security are two important but often contradicting goals in formal specifications.

The flexibility and expressiveness of TOSS are provided by its extended signature mechanism, import/export mechanisms, structured assertions with quantifiers, property modifiers for describing incremental modification of inherited behavior, exception handling mechanism, etc. The security and formality of the language are provided by its state-based formal semantics, control rules for promoting disciplined use of inheritance, and target language independent verification rules which clearly identify process for checking that an implementation conforms to a specification. We believe that TOSS with its set of formal methods can effectively be used in developing reliable object-oriented systems and in constructing a library of reusable specification components.