Uniwersytet Warszawski

Wydział Matematyki, Informatyki i Mechaniki




Małgorzata Górbiel

Nr albumu: 159139



Weryfikacja specyfikacji tropowych
w PVS

na przykładzie uniksowego systemu plików





Praca magisterska
na kierunku INFORMATYKA




Praca wykonana pod kierunkiem
dr J. Mincer-Daszkiewicz
Instytut Informatyki






Październik 2000



Streszczenie


Metoda tropów służy do formalnego specyfikowania interfejsów modułów programistycznych. Do weryfikacji specyfikacji tropowych wybrano system PVS. Specyfikacja jest tłumaczona do języka tego systemu zgodnie z podejściem definicyjnym. Warunki poprawności specyfikacji są generowane przez PVS automatycznie jako obligacje dowodowe.
W ramach pracy przetłumaczono na język systemu PVS zapisaną w metodzie tropów specyfikację uniksowego systemu plików oraz udowodniono większość wygenerowanych przez PVS obligacji dowodowych. Sformułowano zestaw hipotez, które mogą być podstawą walidacji specyfikacji względem oczekiwać użytkownika systemu plików. Przedstawiono również problemy z automatyzacją procesu tłumaczenia i dowodzenia takiej specyfikacji.

Klasyfikacja tematyczna według ACM Computing Classification System:
D.2.4 Software Engineering/Software/Program Verification/Formal Methods
F.3.1 Theory of Computation/Logics and Meaning of Programs/Specifying and Verifying and Reasoning about Programs/Mechanical Verification


Słowa kluczowe: Metoda tropów (TAM), PVS, weryfikacja specyfikacji, walidacja specyfikacji.


Spis treści

  1. Wstęp

  2. Metoda tropów w PVS

    3. 2.1 TAM
    2.2 Tłumaczenie TAM do PVS
    2.3 Weryfikacja poprawności specyfikacj

  3. Specyfikacja uniksowego systemu pików

  4. Przebieg weryfikacji poprawności specyfikacji tropowej uniksowego systemu plików

    5. 4.1 Tłumaczenie do PVS

         4.1.1 Reprezentacja tropu
         4.1.2 Kolejność wyrażeń logicznych
         4.1.3 Poprawność typów w warunku where1
         4.1.4 Funkcje rekurencyjne
         4.1.5 Możliwość automatyzacji procesu tłumaczenia

    4.2 Dowodzenie poprawności specyfikacji

         4.2.1 Typy wygenerowanych TCCs
         4.2.2 Pomocnicze lematy
         4.2.3 Metody dowodzenia
         4.2.4 Dowodzenie TCCs korzystających z funkcji trans

    4.3 Hipotezy
    4.4 Błędy oryginalnej specyfikacji

  5. Podsumowanie


  Literatura


  Dodatek A Przykłady specyfikacji przetłumaczonych do PVS

         A.1 Specyfikacja modułu sequence
         A.2 Specyfikacja modułu inodetable
         A.3 Specyfikacja modułu proces

  Dodatek B Raport z weryfikacji poprawności wybranych modułów