Podsumowanie



Celem pracy było zbadanie praktycznych aspektów opisanej w [1,2,4] metody badania poprawności specyfikacji tropowej przy użyciu systemu PVS. Jako przykład posłużyła zapisana w metodzie tropów specyfikacja uniksowego systemu plików ([5]).

Specyfikacja została przetłumaczona do języka systemu PVS zgodnie z opracowaną metodą. Okazało się jednak, że dowodzenie tak powstałej specyfikacji jest bardzo trudne. Zastosowano więc pewne modyfikacje metody opisane w [6]. Zmodyfikowana metoda uniemożliwiła jednak przetłumaczenie niektórych fragmentów specyfikacji uniksowego systemu plików. Zaproponowane w niniejszej pracy rozszerzenie metody pozwoliło na przetłumaczenie całości specyfikacji interfejsu, bez znacznego skomplikowania dowodów.

Metody dowodzenia okazały się dość ściśle zależne od postaci tropu kanonicznego. Spowodowało to, że proces dowodzenia był bardzo czasochłonny i uciążliwy.

Z 10 modułów, które składały się na specyfikację systemu plików, trzy zostały udowodnione w całości, a dwa w około 90%. Twierdzenia warunkujące poprawność pozostałych modułów, które nie zostały udowodnione automatycznie, zostały jedynie zanalizowane pod kątem ich prawdziwości. Poprawność specyfikacji wymaga jednak ich formalnego udowodnienia, co pozostawiamy jako kontynuację niniejszej pracy. Pomocą w tym mogą okazać się strategie dowodowe, które automatyzują proces dowodzenia. Badaniu możliwości automatyzacji procesu dowodzenia specyfikacji tropowej poświęcone są prace [4,8].

Analizowana specyfikacja tropowa uniksowago systemu plików składa się ze specyfikacji interfejsu i projektu implementacji. Niniejsza praca obejmowała jedynie specyfikację interfejsu. Weryfikacja poprawności projektu implementacji może stanowić temat dalszych prac w tym kierunku.

Z uwagi na zauważone problemy z automatycznym tłumaczeniem (p. 4.1) wydaje się, że w pełni automatyczne tłumaczenie specyfikacji tropowej do PVS nie jest możliwe. Można jednak tak zapisać specyfikację tropową, aby tłumaczenie to było całkowicie automatyczne (p. 4.1.5). W obu przypadkach użycie systemu PVS do weryfikacji poprawności specyfikacji tropowych wydaje sie dobrym rozwiązaniem, gdyż już samo przetłumaczenie specyfikacji do PVS i analiza wygenerowanych warunków poprawności pozwoliła wykryć wiele błędów obecnych w oryginalnej specyfikacji.