Wstęp



Niniejsza praca jest poświęcona zbadaniu możliwości zastosowania systemu PVS do weryfikacji poprawności specyfikacji tropowych.

Metoda tropów (ang. Trace Assertion Method, w skrócie TAM) powstała w 1978 roku jako narzędzie służące do formalnego zapisu specyfikacji modułów programistycznych. Od czasu jej powstania była rozwijana m.in. na naszym Wydziale, co doprowadziło do powstania wersji metody znanej jako TAM'97 ([3]). Obecnie prace nad nią są już właściwie zakończone. W podrozdziale 2.1 zawarto skrócony opis metody potrzebny do zrozumienia dalszej części pracy.

Metoda tropów nie udostępnia mechanizmów kontroli poprawności zapisanej w niej specyfikacji. W celu weryfikacji poprawności specyfikacji tropowej metodę połączono z istniejącym systemem dowodzącym PVS ([7]). Opracowaną metodę tłumaczenia TAM do PVS ([1,2,4]) opisano w podrozdziale 2.2. Przedstawiono tam również pewne modyfikacje metody opisane w pracy [6] i ułatwiające dowodzenie tłumaczonej specyfikacji.

W kolejnym podrozdziale (2.3) przedstawiono sposób użycia systemu PVS do dowodzenia poprawności powstałej specyfikacji.

Opracowane dotychczas przykłady zastosowania opisanej metody do weryfikacji specyfikacji tropowych ograniczały się jedynie do niewielkich przykładów ([1,2,4,6]). Głównym celem niniejszej pracy było zbadanie możliwości zastosowania jej w większych specyfikacjach tropowych. Jako przykład posłużyła specyfikacja uniksowego systemu plików zawarta w obszernej pracy [5], której skrócony opis znajduje się w rozdziale 3.

Opisana w [1] metoda tłumaczenia pozwoliła na przetłumaczenie specyfikacji do PVS, jednak dowodzenie tak powstałej specyfikacji było bardzo trudne. Zastosowanie opisanych w [6] modyfikacji metody znacznie uprościło dowody, jednak pewne jej ograniczenia uniemożliwiły przetłumaczenie niektórych fragmentów specyfikacji. W podrozdziale 4.1 opisano rozwiązanie, które pozwoliło na wyeliminowanie tych trudności nie zwiększając stopnia złożoności dowodów. W podrozdziale tym przedstawiono również inne problemy, które nie pojawiły w dotychczas tłumaczonych specyfikacjach, i sposoby ich rozwiązania.

Najtrudniejszą częścią pracy było przeprowadzenie dowodów. Metodom dowodzenia poświęcono podrozdział 4.2.

W podrozdziale 4.3 opisano dołączone do specyfikacji hipotezy, które pozwoliły na jej walidację.

Błędy wykryte w trakcie procesu weryfikacji specyfikacji opisano w podrozdziale 4.4.

Wyniki pracy w postaci przetłumaczonej do PVS specyfikacji uniksowego systemu plików, łącznie z dowodami, znajdują się na dołączonej do pracy dyskietce. Specyfikacje wybranych modułów w PVS można znaleźć w dodatku A. Dodatek B zawiera raport z weryfikacji poprawności wybranych modułow: wykaz wygenerowanych dla modułu TCCs wraz z informacją o tym na jakim etapie znajduje się każdy dowód (ang. Proof summary).

Pragnę gorąco podziękować dr Janinie Mincer-Daszkiewicz za nieocenioną pomoc przy tworzeniu tej pracy.

Dziękuję również mgrowi Marcinowi Engelowi za cenne uwagi merytoryczne dotyczące pracy.