Transforming architectural descriptions of component-based systems for formal analysis

Design time analysis is an important step in the process of developing software systems, with the goal of ensuring that the system design conforms to the design constraints that are stated as part of the functional and non-functional requirements. The well-known techniques for formally analyzing a design are model checking, axiom-based formal verification, and real-time schedulability analysis that takes into account resource constraints. In this thesis, model checking and real-time schedulability are the techniques used to verify that the system under development is both safe and secure. The architecture of a trustworthy system, formally described in Trustworthy Architectural Description Language (TADL), is taken as the input for the analysis stage. Instead of developing new tools to perform the analyses, the thesis has developed transformation techniques to transform TADL descriptions into behaviour protocols used by existing verification tools. The transformation rules are described independently of the transformation process, thus allowing both reuse and easy extendability. A tool based on such techniques has been designed and implemented which automatically generates two types of models from a TADL description. One is the UPPAAL model, on which the security and safety properties of the system under design are formally verified. The second output is the TIMES model, on which real-time schedulability analysis is performed. The techniques and tools are applied to The Common Component Modelling Example (CoCoME), a case study defined by the component development community, to demonstrate that TADL is expressive enough to formally describe component-based systems