Formalizacja i sprawdzanie modeli stylu architektury oprogramowania

W niniejszym badaniu opisano formalne modele systemu ATM przy użyciu języków opartych na stanach takich jak Z B i Alloy a także języka opartego na zdarzeniach takiego jak Monterey Phoenix. Sprawdzanie modeli odbywa się za pomocą zautomatyzowanych narzędzi tj. Z/EVES Atelier B i Alloy Analyzer dla specyfikacji Z B i Alloy. Ponadto przedstawiono analizę porównawczą różnych cech charakterystycznych dla różnych podejść formalnych. Architektura oprogramowania odgrywa ważną rolę w projektowaniu wysokopoziomowym systemu pod względem komponentów łączników i konfiguracji. Głównym elementem składowym architektury oprogramowania jest styl architektoniczny który zapewnia semantykę projektowania specyficzną dla danej dziedziny. W analizie złożonego stylu architektonicznego podjęto próbę sformalizowania jednego złożonego stylu np. C2 (komponent i łącznik) przy użyciu formalnego języka specyfikacji Alloy. Do sprawdzania spójności notacji modelowania wykorzystuje się narzędzie do sprawdzania modeli np. Alloy Analyzer.