Niezawodne Systemy Informatyczne

Stacks Image 3001

Bombowiec B-1B (fot. avioners.net)

Formal methods should be part of the education of every computer scientist and software engineer, just as the appropriate branch of applied maths is a necessary part of the education of all other engineers.
Z raportu FAA (Federal Aviation Authority) i NASA
NVIDIA's selection of Ada and SPARK ushers in a new era in the history of safety- and security-critical software development.
Quentin Ochem

Aktualności

25.05.2021 dzisiaj na stronie adacore.com/download pojawiła się nowa wersja GNAT 2021

Opis kursu

Moduł wprowadzający w zagadnienia związane z tworzeniem systemów co do których stawia się krytyczne wymagania. Wykłady rozpoczynają się wstępem dotyczącym niezawodności oprogramowania i sprzętu. Następnie omawiane są narzędzia wspierające weryfikację poprawności programów stworzone dla języka Ada, który znajduje zastosowanie w systemach o znaczeniu krytycznym. Przedstawione zostaje również projektowanie kontraktowe wraz z przykładami jego wykorzystania w wybranych językach programowania. Podczas zajęć laboratoryjnych rozwiązywane są zadania dzięki którym nabywa się praktycznej umiejętności stosowania narzędzi omawianych na wykładach.

Zasady zaliczenia

  • Ocena z grupy kursów wyliczana jest na podstawie średniej ważonej z punktów uzyskanych na laboratorium i na kartkówkach.
  • Aby zaliczyć grupę kursów należy uzyskać co najmniej 50 punktów z laboratorium i co najmniej 50 punktów z kartkówek.
  • Progi ocen zamieszczono poniżej w postaci kontraktu procedury Oblicz_Zaliczenie.
  • Kartkówki odbędą się na ostatnich wykładach w semestrze (terminy i tematy zostaną podane wkrótce).
  • Listy zadań na laboratoriach należy rozwiązywać samodzielnie i zaliczać w terminie podanym przy każdej liście.
  • Laboratorium musi być zaliczone do 15-go tygodnia zajęć (nie ma możliwości zaliczania laboratorium w sesji egzaminacyjnej).
  • Przy każdym zadaniu na liście zadań podano maksymalną liczbę punktów jaką można za nie otrzymać.
  • Liczba punktów otrzymywanych za zadanie zależy od tego, które warunki udało się programowi gnatprove automatycznie udowodnić.
  • Kryteria wyliczania liczby punktów podano na wstępie do każdej listy zadań.
procedure Oblicz_Zaliczenie(LAB: in Float; KOL: in Float; ZAL: out Float)
with
  Pre =>
    LAB >= 50.0 and LAB <= 100.0 and KOL >= 50.0 and KOL <= 100.0,
  Contract_Cases =>
    (
      0.4*LAB + 0.6*KOL < 50.0 => ZAL = 2.0,
      0.4*LAB + 0.6*KOL < 60.0 => ZAL = 3.0,
      0.4*LAB + 0.6*KOL < 70.0 => ZAL = 3.5,
      0.4*LAB + 0.6*KOL < 80.0 => ZAL = 4.0,
      0.4*LAB + 0.6*KOL < 90.0 => ZAL = 4.5,
      others                   => ZAL = 5.0
    );

Plan wykładu

1 Wstęp (2h)

2-8 SPARK (14h)

  • Elementy języka SPARK
  • Pakiety
  • Sprawdzanie zaleźności
  • Dowodzenie

9-11 Metody formalne (6h)

  • Weryfikacja programów while
  • Analiza przepływu sterowania
  • Analiza przepływu danych

12-13 Systemy krytyczne (4h)

  • Pewność
  • Specyfikowanie systemów krytycznych
  • Wytwarzanie systemów krytycznych

14 Przegląd innych narzędzi (2h)

  • Frama-C dla języka C
  • KeY dla Java

15 Podsumowanie (2h)

Prezentacja

Wybrane przykłady prezentowane na wykładzie można znaleźć w repozytorium przemko/ada-spark-nsi.

Terminy kartkówek

Literatura

SPARK

Metody formalne

Niezawodność

Dziesięć fundamentalnych zasad

Poniższe zasady pochodzą z artykułu Gerarda Holzmanna The Power of 10: Rules for Developing Safety-Critical Code:
  1. Ogranicz cały kod do bardzo prostych konstrukcji sterujących -- nie używaj instrukcji goto, konstrukcji setjmp lub longjmp ani bezpośredniej lub pośredniej rekurencji.
  2. W każdej pętli podawaj stały górny zakres.
  3. Nie używaj dynamicznej alokacji pamięci po zainicjowaniu.
  4. Żadna funkcja nie powinna być dłuższa na wydruku niż jedna strona papieru, przy standardowym formatowaniu z jednym wierszem na instrukcję i jednym wierszem na deklarację.
  5. Średnia liczba asercji w kodzie powinna wynosić co najmniej dwie na jedną funkcję.
  6. Deklaruj wszystkie obiekty danych w najwęższym możliwym zakresie.
  7. Każde wywołanie funkcji musi sprawdzać zwracaną przez funkcję wartość a każda wywołana funkcja musi sprawdzać poprawność wartości wszystkich parametrów dostarczonych w wywołaniu.
  8. Użycie preprocesora musi ograniczać się jedynie do dołączania plików nagłówkowych i prostych makrodefinicji.
  9. Użycie wskaźników musi być ograniczone. W szczególności poziom dereferencji nie może być większy niż jeden.
  10. Cały kod musi być kompilowany od pierwszego dnia rozwijania z ostrzeżeniami kompilatora na jak najbardziej pedantycznym poziomie. Cały kod musi kompilować się bez żadnych ostrzeżeń.

Odnośniki do stron

Przykłady projektów w języku SPARK

Narzędzia

Opis instalacji narzędzi w przypadku systemu Linux:
  1. Ściągnij plik gnat-2020-20200818-x86_64-linux-bin ze strony https://www.adacore.com/download/
  2. Ustaw flagę wykonywania dla ściągniętego pliku: chmod +x gnat-2020-20200818-x86_64-linux-bin
  3. Uruchom ściągnięty plik: ./gnat-2020-20200818-x86_64-linux-bin
  4. Nie zapomnij dopisać ścieżkę do katalogu GNAT/2020/bin w zmiennej środowiskowej PATH.
  5. Być może zaistnieje potrzeba doinstalowania pewnych pakietów (np. pod Debian 10 musiałem doinstalować pakiet libncurses5).
  6. Przeczytaj o ustawieniu zmiennej środowiskowej GPR_PROJECT_PATH w dokumentacji: https://docs.adacore.com/spark2014-docs/html/ug/en/install.html

Przykład weryfikacji

Załóżmy, że w pliku test.adb znajduje się następujący kod:
procedure Test with SPARK_Mode is
  X : Integer;
begin
  X := 2 + 2;
  pragma Assert (X = 4);
end Test;

natomiast w pliku test.gpr następujący opis projektu:
project Test is
  for Main use ("test.adb");
end Test;


Aby zweryfikować poprawność procedury Test, należy wydać następujące polecenie:
$ gnatprove -P test.gpr
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Summary logged in /Users/przemko/gnatprove/gnatprove.out


Pliki powstałe podczas weryfikacji znalazły się w podkatalogu gnatprove. Raport z weryfikacji został zamieszczony w pliku gnatprove/gnatprove.out:
$ more gnatprove/gnatprove.out
Summary of SPARK analysis
=========================

-------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total       Flow   Interval   CodePeer     Provers   Justified   Unproved
-------------------------------------------------------------------------------------------------------
Data Dependencies                 .          .          .          .           .           .          .
Flow Dependencies                 .          .          .          .           .           .          .
Initialization                    1          1          .          .           .           .          .
Non-Aliasing                      .          .          .          .           .           .          .
Run-time Checks                   .          .          .          .           .           .          .
Assertions                        1          .          .          .    1 (CVC4)           .          .
Functional Contracts              .          .          .          .           .           .          .
LSP Verification                  .          .          .          .           .           .          .
-------------------------------------------------------------------------------------------------------
Total                             2    1 (50%)          .          .     1 (50%)           .          .


Analyzed 1 unit
in unit test, 1 subprograms and packages out of 1 analyzed
  Test at test.adb:3 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (1 checks)

Aby posprzątać po weryfikacji należy wykonać następujące polecenie:
$ gnatprove -P test.gpr --clean

Listy zadań

Rozwiąż samodzielnie poniższe listy zadań:

Wskazówki

Czasami istnieje konieczność dopisania w programie asercji, które umożliwią automatyczne udowodnienie poprawności programu.

Na przykład, w zadaniu o schemacie Hornera można pomyśleć o takiej asercji:

pragma Assert (for all A in Integer => (for all B in Positive => A ** B = A * A ** (B - 1) ));

Wady częściowej poprawności

Stacks Image 9609