3.03.2005

Specyfikacje architekturalne i ich weryfikacja

Referat zawierac bedzie ogolny zarys i glowne wyniki mojej pracy doktorskiej. Praca ta poswiecona jest badaniu _specyfikacji architekturalnych_ --- formalizmu, ktory sluzy do opisu modularnej struktury procesu budowy oprogramowania.

W pierwszej czesci pracy definiujemy i analizujemy pojecie specyfikacji architekturalnej. Rozwazamy miedzy innymi rozne odmiany semantyki tych specyfikacji. Badamy takze stosunek miedzy formalizacja procesu budowania oprogramowania dokonana w sposob posredni, na modelach (algebrach) danej logiki, a formalizacja dokonana bezposrednio na programach. Wprowadzamy pojecie w pelni statycznej poprawnosci, ktore mozna stosowac do jezykow specyfikacji majacych wlasnosc amalgamacji. W pelni statyczna poprawnosc zapewnia, ze proces budowania oprogramowania poprawny na poziomie modeli jest tez poprawny na poziomie programow.

Druga czesc rozprawy poswiecona jest _weryfikacji_ specyfikacji architekturalnych, tzn. dowodzeniu, ze opisany przez taka specyfikacje proces budowy oprogramowania jest poprawny. Wprowadzamy poprawny i (wzglednie) zupelny rachunek logiczny sluzacy weryfikacji w pelni statycznych specyfikacji architekturalnych. Poniewaz np. jezyk specyfikacji CASL nie ma wlasnosci amalgamacji, przedstawiamy takze dwie poprawne i zupelne metody weryfikacji dla jezykow bez tej wlasnosci. Obie metody opieraja sie na reprezentacji interesujacego nas jezyka specyfikacji w innym jezyku, posiadajacym wlasnosc amalgamacji i spelniajacym pewne dalsze warunki. Metody te roznia sie tym, ze jedna polega na statycznych wlasnosciach specyfikacji, podczas gdy druga niemal calkowicie te wlasnosci pomija.