Niezawodne systemy informatyczne (W04INA-SI0835G)

Stacks Image 9617
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

Wstęp (2h)

SPARK (14h)

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

Metody formalne (6h)

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

Systemy krytyczne (4h)

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

Przegląd innych narzędzi (2h)

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

Kolokwium (2h)

Prezentacja

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

Terminy kartkówek

TBA

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. Zainstaluj zarządcę pakietów Alire
  2. Po zainicjowaniu nowego pakietu przejdź do jego katalogu
  3. Zdefiniuj zależność za pomocą polecenia alr with gnatprove
  4. Wykonaj analizę kodu za pomocą polecenia alr gnatprove

Przykład weryfikacji

Zainicjuj nowy pakiet test:
alr init --bin test
Przejdź do katalogu test i wpisz do pliku src/test.adb następujący kod:
procedure Test with SPARK_Mode is
  X : Integer;
begin
  X := 2 + 2;
  pragma Assert (X = 4);
end Test;
Zdefiniuj następującą zależność:
alr with gnatprove
Aby zweryfikować poprawność procedury Test, należy wydać następujące polecenie:
alr gnatprove --report=all
Wynik analizy:
Stacks Image 9654
Pliki powstałe podczas weryfikacji znalazły się w podkatalogu obj/development/gnatprove. Raport z weryfikacji został zamieszczony w pliku gnatprove.out:
cat obj/development/gnatprove/gnatprove.out 
Summary of SPARK analysis
=========================

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


max steps used for successful proof: 1

Analyzed 1 unit
in unit test, 1 subprograms and packages out of 1 analyzed
  Test at test.adb:1 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Aby posprzątać po weryfikacji należy wykonać następujące polecenie:
alr gnatprove --clean

Listy zadań

Rozwiąż samodzielnie poniższe listy zadań:
TBA

Wskazówka

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

Sprawdzenie częściowej poprawności programu nie gwarantuje jego poprawności w przypadku gdy nie kończy on pracy. Pamiętaj aby dla każdej pętli podać za pomocą pragmy Loop_Variant wielkość, której zmiana gwarantuje zakończenie pętli.

Poniżej zamieszczono przykład kodu, dla którego można udowodnić asercję ewidentnie fałszywą. Wynika to z tego, że niekończący się program spełnia każdy warunek zakończenia — również fałszywy. 
procedure Schrodinger with SPARK_Mode is
   Cat_Is_Dead : Boolean := False with Ghost;
begin
   loop
      null;
   end loop;
   pragma Assert ( Cat_Is_Dead and not Cat_Is_Dead );
end Schrodinger;