W ostatnim poście dzieliłem się wrażeniami z konferencji Ada Europe 2019, która miała miejsce 12 i 13 czerwca w Warszawie. Tekst wyszedł dosyć długi i zabrakło w nim miejsca na opis poszczególnych prezentacji, które dodaję dzisiaj. Podczas konferencji można było między innymi usłyszeć o wojskowym projekcie tak tajnym, że nie można o nim mówić, o rakiecie Ariane 6, czy o nowościach w Ada 2020. Zapraszam do lektury!

Contract based design in SPARK

Ta prezentacja przykuła moją uwagę praktycznie od samego początku, kiedy padły mniej więcej takie słowa:

Prezentację opieram na swoich doświadczeniach z projektu dla armii brytyjskiej. Niestety nie mogę o nim zająknąć się ani słowem, dlatego przedstawię ten sam problem na przykładzie sterowania podgrzewaniem wody.

Prezentacja porównywała Test Driven Development (TDD) z Design By Contract (DbC).

Przed implementacją oczywiście musiały być sformułowane wymagania i do tego posłużył SCADE. Projekt był tworzony zgodnie z Model Based Design. Ta metoda często przewijała się w trakcie konferencji i pewnie zrobię o tym dedykowany wpis. W skrócie chodzi o to, żeby pracować na abstrakcyjnym modelu z którego później jest generowany kod. Taki model można również łatwo przenieść np. do symulacji. W Model Based Design zwykle używa się maszyn stanu do opisu działania systemu.

Korzystając z TDD wychodzimy od wymagań, piszemy test i dodajemy implementację. Musimy jednocześnie spełnić wymagania norm dotyczące między innymi traceability. Musimy więc być w stanie zmapować konkretne wymagania na testy i na kod. Było to robione ręcznie za pomocą review. Reviewer musiał więc wykonać oddzielnie sprawdzenie zgodności z wymaganiami kodu i testów.

W podejściu DbC z modelu zostały wygenerowane kontrakty. Dużą pomocą było tu wykorzystanie języka Spark umożliwiającego sprawdzenie ich poprawności w czasie kompilacji. Normalnie w DbC umieszczamy w kodzie asercje, które działają dopiero w runtime, więc i tak musimy wszystkie ścieżki przetestować. Spark może zakończyć kompilację błędem jeśli kontrakty są niespełnione, dzięki czemu nie musimy pisać na nie testów.

Kontrakty były automatycznie generowane ze SCADE. Jako, że tool miał certyfikację, można było pominąć manualną weryfikację. Umożliwiało to zaoszczędzenie czasu. Oczywiście normy dalej wymagają pełnego code coverage, więc unit testy w dalszym ciągu trzeba robić. Jednak przenosząc część pracy na kompilator prawdopodobnie możliwe były oszczędności.

Kontrakty były automatycznie generowane ze SCADE, przez co ich czytelność dla zwykłego śmiertelnika pozostawiała wiele do życzenia:

Kontrakty wyglądają tutaj na kopię ifów wykorzystywanych później w kodzie. Więc są rodzajem duplikacji. Na pewno sprawdzanie ich podczas kompilacji jest kuszące, ale jak widać mają również wady.

Ariane 6

Inna bardzo ciekawa prezentacja zdradzała nieco kulisy powstawania rakiety Ariane 6 w Europejskiej Agencji Kosmicznej.

Po raz kolejny przewijało się Model Based Design i maszyny stanów. W ESA jednak używają do tego SysML. Wyróżniają tam 4 rodzaje kodu:

  • generyczne biblioteki np. matematyczne,
  • kod generowany automatycznie z SysML,
  • algorytmy pisane przez programistów,
  • pozostały kod pisany przez programistów.

Kod jest pisany w Adzie 2012. Generatory z modeli SysML nie są certyfikowane, więc muszą być walidowane ręcznie.

Model Based Design umożliwia im łatwe przenoszenie projektu do środowiska symulacyjnego, gdzie mogą go poddawać różnym testom. Mają również procedury zapewniające odpowiednią zgodność symulacji z rzeczywistymi warunkami.

Teaching Ada

Ta prezentacja odbyła się na koniec pierwszego dnia i była prowadzona przez Jean-Pierre Rosena, który ma już 40 lat doświadczenia w szkoleniu z Ady. Szkolenia prowadził jeszcze zanim ukazał się pierwszy standard Ada83.

Nauka Ady wymaga zmiany myślenia. Dużo nawyków z innych języków nam przeszkadza. Wiele konstrukcji jest specyficznych tylko dla Ady np. discriminants czyli struktury z zawartością zależną od argumentu. Kompilator nie przepuszcza nam wielu błędów, które normalnie byśmy musieli debugować. Musimy więc często kompilować, żeby usuwać te błędy na bieżąco.

Konkluzja była taka, że dzisiaj nie uczy się solidnych program Software Engineeringu. Zamiast tego jest nacisk na jak najszybsze efekty. Mamy więc Agile, Rapid development i minimalizację time to market. W efekcie otrzymujemy programy pełne błędów i trudne w utrzymaniu.

Ada 2020

Keynote drugiego dnia prowadził Tucker Taft odpowiedzialny za nowe wersje standardów Ady. Prezentacja dotyczyła standardu, który ma wyjść w przyszłym roku. Będą one dotyczyć głównie wsparcia dla programowania współbieżnego w tym GPU, dojdą też elementy programowania funkcyjnego. Chociaż brzmi to głupio, Ada upodobni się trochę do Pythona. Dojdzie coś w stylu list comprehension:

Przy zmianach dotyczących współbieżności Ada współpracuje z OpenMP, którego przedstawiciel miał keynote pierwszego dnia. OpenMP to rozszerzenie kompilatorów C i C++ umożliwiające dodawanie pragm do wykonywania fragmentów kodu na GPU. Dzięki temu możemy pisać całą aplikację w natywnym C zamiast w CUDA, czy OpenCL.

Ada na ROS

ROS czyli Robot Operating System to temat mi bliski. Autor prezentacji pokazywał postępy prac nad RCLAda umożliwiającym pisanie węzłów ROS w Adzie. Oczywiście safety-critical w ten sposób nie osiągniemy, ale otwiera to możliwości pisania z większą ilością checków w czasie kompilacji. Rozwój projektu można śledzić na GitHubie.

Prezentacje sponsorów

Zwykle prezentacje sponsorów to głównie marketingowy bełkot. Tym razem jednak byłem bardzo pozytywnie zaskoczony. Szczególnie podobała mi się prezentacja Vectora o testowaniu. Ich flagowym produktem jest narzędzie do unit testów VectorCast, które jest trochę wypaczeniem idei TDD. Jednak sama prezentacja była świetna i zawierała wiele złotych myśli.

Testy są jak ubezpieczenia:

Pisanie testów na podstawie kodu, a nie wymagań, jest jak tworzenie klucza odpowiedzi do egzaminu na podstawie odpowiedzi studenta:

Prezentacje akademickie

Podczas konferencji było sporo prelekcji o badaniach na różnych uniwersytetach. Główne obszary to schedulery, systemy czasu rzeczywistego, analiza worst case execution time (WCET). Było także o systemach mixed criticality – czyli takich, gdzie różne moduły mają różne poziomy SIL. Poziom tych prezentacji był dosyć nierówny. Część była fajna, ale trafiały się też nudne.

Podsumowanie

Jak widać prezentacje dotykały tematów, których próżno szukać na innych konferencjach. I nie chodzi mi tutaj o język Ada, tylko bardziej o rodzaje problemów i tworzonych systemów. Bo nawet nie programując w Adzie można było wyciągnąć dużo wniosków do wykorzystania w innych projektach safety-critical.