A Modular Method for High- Level Service Specification and Component Design Derivation

Abstract

This thesis addresses the problem of specifying the behaviour of distributed reactive systems in such a way that the component behaviours can be derived automatically. This automation demands specifications to be complete in the sense that they fully define all desired behaviours. Achieving completeness is not trivial due to independence and concurrency among interfaces and components. This tends to generate very large possible event orderings rendering complete specifications impractical using the common event oriented specification languages like sequence diagrams. This situation is addressed by the key research question of this thesis: “Can we define an improved method that helps to achieve necessary completeness and modularity in global behaviour specifications?”. The first part of the question deals with completeness of specifications. This thesis proposes that complete specifications should cover not only interactions among concurrent parts but also data and operations (the core) that are important for the users and the environment of a system. The second part of the question deals with modularity in specifications. Modularity, widely considered as a mechanism for improving flexibility and comprehensibility of systems development, is achieved by the separation of interface specifications from the core and defining them in separate modules. The decomposition of specifications has resulted in an improved method, namely “The Interface-Modular (IM) Method” (the main contribution of this thesis), for global behaviour specifications of distributed reactive systems. The IM method achieves the necessary completeness, rigour and modularity needed for automatic component derivation by: (1) defining both the interface functionality (interactions among concurrent parts) and the core functionality (data and operations, and their ordering); (2) factorizing the interface functionality and the core functionality into separate modules that have connectors to enable composition of the global behaviour specifications; (3) explicitly specifying the dependencies among the modules; (4) using UML activity diagrams in combination with collaborations that support syntax and semantics for modular specifications; (5) modelling role instance multiplicity in interface specifications; (6) defining session initiation functionality to deal with dynamic links among multiple instances; (7) providing precise guidelines for realization of global behaviours using look-up tables; (8) proposing modular solutions for known realizability problems; and (9) forming step-wise guidelines for deriving detailed component designs. The research is evaluated and demonstrated by using TaxiSystem as a case study. The realizability resolution modules proposed are validated for their consistency by implementing them in a tool (Reactive Blocks) that formally analyses the specifications by means of model checking. We expect the IM method to facilitate the process of automatic component derivation by enabling the designers: to specify complete global behaviours using modular specifications (that is composed of modules that can be understood and analysed separately); to detect the realizability problems early in the specifications; and to apply the realizability resolutions in a modular way.