Specifications of Software Architectures using Diagrams of Constructions
Grzegorz Marczyński · 2014
Formal methods promise the ultimate quality of software artifacts with mathematical proof of their correctness. Algebraic specification is one of such methods, providing formal specifications of system components suitable for verification of correctness of all individual steps in the software development process, and hence of the entire development process and of the resulting program. In this thesis we propose a new approach to algebraic specifications of software architectures, called diagrams of construction specifications. Constructions, as introduced here, model parameterised modules, with dependency relation captured directly on signature symbols. They give a uniform treatment of firstand higher-order parameterisation, and are equipped with a single sum operation which subsumes the most standard operations on parameterised modules. We introduce specifications for such constructions, study their compositionality properties, and define a notion of refinement for constructor specifications. Diagrams of construction specifications capture design and development of modular software architecture, based on decomposition and refinement of construction specifications. Throughout the thesis we illustrate new concepts and problems discussed by means of simple examples; a somewhat longer example is also added to summarize our presen-