Opis
Książka została podzielona na dziesięć rozdziałów, zawiera także trzy dodatki. Informacje wprowadzające do omawianej tematyki oraz potrzebne do zrozumienia dalszej części książki przedstawione są krótko w rozdziale drugim i trzecim.
Rozdział drugi prezentuje wybrane zagadnienia dotyczące formalnej specyfikacji sterownika logicznego. Jako forma specyfikacji sterownika logicznego została wybrana sieć Petriego (interpretowania sieć Petriego sterowania), poprzedzona wprowadzeniem do alternatywnej formy – algorytmicznych maszyn stanów ASM. Rozdział trzeci prezentuje wybrane zagadnienia dotyczące formalnej weryfikacji modelowej, skupiając się na krótkiej prezentacji logiki temporalnej i jej podstawowych założeń oraz na samej technice weryfikacji modelowej. Ponadto został przedstawiony istniejący stan wiedzy dotyczący badanej tematyki. Opisano wybrane narzędzie wnioskowania komputerowego (NuSMV) wykorzystywane w dalszych badaniach.
Rozdział czwarty, piąty, szósty i siódmy omawia opracowane nowatorskie metody i prezentuje uzyskane wyniki badań.
Proponowane metody formalnej weryfikacji modelowej algorytmicznych maszyn stanów oraz sieci Petriego zostały przedstawione w rozdziale czwartym. Nowatorskie podejście do weryfikacji formalnej specyfikacji behawioralnej sterownika (omówione krótko pod koniec rozdziału), wprowadzające regułowy model logiczny, uszczegółowiono w następnych rozdziałach.
Rozdział piąty omawia zasady tworzenia modelu logicznego opisującego w regułowy sposób działanie sterownika logicznego wyrażonego za pomocą interpretowanej sieci Petriego sterowania. Z kolei sposób weryfikacji modelowej modelu logicznego został przedstawiony w rozdziale szóstym. Następnie zaprezentowano zasady syntezy logicznej zweryfikowanego wcześniej modelu.
Rozdział ósmy zawiera przykłady formalnej weryfikacji specyfikacji programów. Weryfikowana jest specyfikacja w postaci algorytmicznej maszyny stanów oraz sieci Petriego, a także specyfikacja behawioralna przedstawiona w formie regułowej (przykład ilustrujący krok po kroku zastosowanie opracowanych metod wspomagających pracę projektanta i pozwalających na podniesienie jakości produktu końcowego). Przykłady zostały zweryfikowane przy wykorzystaniu narzędzia NuSMV w wersji 2.5.2.
Rozdział dziewiąty krótko opisuje oprogramowanie zrealizowane na potrzeby badań, automatyzujące proces transformacji modelu logicznego do modelu weryfikowalnego oraz modelu syntezowalnego. Przedstawiono interfejs użytkownika oraz sposób korzystania z aplikacji.
Rozdział dziesiąty podsumowuje wyniki badań. Wskazuje elementy nowatorskie pracy, jej rezultat oraz plany dalszych badań.
Dodatek A zawiera dwa przykładowe pliki w języku opisu sprzętu VHDL utworzone na podstawie opracowanego modelu logicznego. Dodatek B stanowi polsko-angielski słownik najczęściej wykorzystywanych terminów pojawiających się w książce. Dodatek C natomiast zawiera najczęściej wykorzystywane skróty.
Monografia powstała na podstawie rozprawy doktorskiej autorki.
