Specifications of Software Architectures using Diagrams of Constructions

Metody formalne umożliwiają uzyskanie najwyższej jakości procesu wytwarzania oprogramowaniaprzez dostarczenie matematycznych dowodów jego poprawności. Jedną ztakich metod są specyfikacje algebraiczne, które podają sposób formalnej specyfikacjiposzczególnych komponentów systemu informatycznego oraz weryfikacji poprawnościwszystkich kroków procesu wytwarzania oprogramowania i w rezultacie dają możliwośćzapewnienia poprawności zarówno całego procesu, jak i samego wynikowego programu.W niniejszej rozprawie proponuje się nowe podejście do algebraicznych specyfikacji architekturoprogramowania zwane diagramami specyfikacji konstrukcji. Wprowadzonejest pojęcie konstrukcji, które są modelami sparametryzowanych modułów wraz z relacjązależności wyrażoną bezpośrednio na symbolach z ich sygnatur. Konstrukcjezapewniają jednolite podejście do parametryzacji pierwszego i wyższych rzędów. Jedynąoperacją na konstrukcjach jest suma, która z powodzeniem zastępuje większośćstandardowych operacji na modułach sparametryzowanych. W rozprawie przedstawianesą specyfikacje konstrukcji, przeprowadzane są badania ich kompozycjonalnościoraz definiowane jest pojęcie uściślenia (ang. refinement) specyfikacji konstrukcji. Diagramyspecyfikacji konstrukcji pozwalają modelować strukturę i rozwój modularnycharchitektur oprogramowania opartych na dekompozycji i uściślaniu specyfikacji konstrukcji.W całym tekście podawane są liczne małe przykłady wprowadzanych pojęć i dyskutowanychproblemów. Na koniec przytoczony jest nieco dłuższy przykład ilustrującykilka kroków rozwoju architektury prostego systemu informatycznego.

Formal methods promise the ultimate quality of software artifacts with mathematicalproof of their correctness. Algebraic specification is one of such methods, providingformal specifications of system components suitable for verification of correctnessof all individual steps in the software development process, and hence of the entiredevelopment 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 introducedhere, model parameterised modules, with dependency relation captured directly onsignature symbols. They give a uniform treatment of first- and higher-order parameterisation,and are equipped with a single sum operation which subsumes the moststandard operations on parameterised modules. We introduce specifications for suchconstructions, study their compositionality properties, and define a notion of refinementfor constructor specifications. Diagrams of construction specifications capturedesign and development of modular software architecture, based on decomposition andrefinement of construction specifications.Throughout the thesis we illustrate new concepts and problems discussed by means ofsimple examples; a somewhat longer example is also added to summarize our presentation.