Budowa i analiza procesów rozproszonych

Budowa i analiza procesów rozproszonych
Deweloperzy	INRIA CONVECS (dawniej zespół VASY )
Pierwsze wydanie	1989, 33–34 lata temu
Wersja stabilna	2023 / 13 lutego 2023 ; 19 dni temu
System operacyjny	Windows , macOS , Linux , Solaris i OpenIndiana
Typ	Zestaw narzędzi do projektowania protokołów komunikacyjnych i systemów rozproszonych
Strona internetowa	cadp .inria .fr

CADP (Construction and Analysis of Distributed Processes) to zestaw narzędzi do projektowania protokołów komunikacyjnych i systemów rozproszonych. CADP jest rozwijany przez zespół CONVECS (wcześniej przez zespół VASY) w firmie INRIA Rhone-Alpes i połączony z różnymi dodatkowymi narzędziami. CADP jest utrzymywany, regularnie ulepszany i używany w wielu projektach przemysłowych.

Celem zestawu narzędzi CADP jest ułatwienie projektowania niezawodnych systemów poprzez wykorzystanie formalnych technik opisu wraz z narzędziami programowymi do symulacji, szybkiego tworzenia aplikacji , weryfikacji i generowania testów.

CADP można zastosować do dowolnego systemu, który obejmuje współbieżność asynchroniczną, tj. dowolnego systemu, którego zachowanie można modelować jako zestaw równoległych procesów zarządzanych przez semantykę przeplatania. Dlatego CADP może być używany do projektowania architektury sprzętowej, algorytmów rozproszonych, protokołów telekomunikacyjnych itp. Techniki weryfikacji enumeratywnej (znanej również jako jawna weryfikacja stanu) zaimplementowane w CADP, choć mniej ogólne niż dowodzenie twierdzeń, umożliwiają automatyczne, efektywne kosztowo wykrywanie błędów projektowych w złożonych systemach.

CADP zawiera narzędzia wspierające wykorzystanie dwóch podejść w metodach formalnych, z których oba są potrzebne do niezawodnego projektowania systemów:

Modele zapewniają matematyczne reprezentacje programów równoległych i powiązanych problemów weryfikacyjnych. Przykładami modeli są automaty, sieci automatów komunikujących się, sieci Petriego, binarne diagramy decyzyjne, układy równań boolowskich itp. Z teoretycznego punktu widzenia badanie modeli ma na celu uzyskanie wyników ogólnych, niezależnych od określonego języka opisu.
W praktyce modele są często zbyt elementarne, aby bezpośrednio opisywać złożone systemy (byłoby to żmudne i podatne na błędy). Do tego zadania potrzebny jest formalizm wyższego poziomu, zwany algebrą procesów lub rachunkiem procesów , a także kompilatory, które tłumaczą opisy wysokiego poziomu na modele odpowiednie dla algorytmów weryfikacyjnych.

Historia

Prace nad CADP rozpoczęto w 1986 r., kiedy podjęto prace nad dwoma pierwszymi narzędziami, CAESAR i ALDEBARAN. W 1989 roku powstał akronim CADP, który oznacza pakiet dystrybucyjny CAESAR/ALDEBARAN . Z biegiem czasu dodano kilka narzędzi, w tym interfejsy programistyczne, które umożliwiły współtworzenie narzędzi: akronim CADP stał się następnie pakietem programistycznym CAESAR/ALDEBARAN . Obecnie CADP zawiera ponad 50 narzędzi. Zachowując ten sam akronim, zmieniono nazwę zestawu narzędzi, aby lepiej wskazywała na jego przeznaczenie: Konstrukcja i analiza procesów rozproszonych .

Główne wydania

Wersje CADP zostały nazwane kolejno literami alfabetu (od „A” do „Z”), następnie nazwami miast, w których działają akademickie koła naukowe aktywnie pracujące nad językiem LOTOS, a ogólniej nazwami miast, w których główne wniesiono wkład w teorię współbieżności .

Kryptonim	Data
"A" ... "Z"	styczeń 1990 - grudzień 1996
Twente	czerwiec 1997 r
Lenny	styczeń 1999 r
Ottawa	lipiec 2001
Edynburg	grudzień 2006
Zurych	Grudzień 2013
Amsterdam	grudzień 2014 r
Kamienny Potok	grudzień 2015 r
Oksford	grudzień 2016 r
Zofia Antipolis	grudzień 2017 r
Uppsala	grudzień 2018 r
Piza	grudzień 2019 r
Aalborg	grudzień 2020 r
Saarbrücken	grudzień 2021 r
Kista	grudzień 2022 r
Akwizgran	luty 2023 r

Pomiędzy głównymi wersjami często dostępne są mniejsze wersje, zapewniające wczesny dostęp do nowych funkcji i ulepszeń. Więcej informacji można znaleźć na listy zmian w witrynie CADP.

Funkcje CADP

CADP oferuje szeroki zestaw funkcji, począwszy od symulacji krok po kroku, aż po masowo równoległe sprawdzanie modeli . Obejmuje:

Kompilatory dla kilku formalizmów wejściowych:
- Opisy protokołów wysokiego poziomu napisane w języku ISO LOTOS . Zestaw narzędzi zawiera dwa kompilatory (CAESAR i CAESAR.ADT), które tłumaczą opisy LOTOS na kod C, który można wykorzystać do celów symulacji, weryfikacji i testowania.
- Opisy protokołów niskiego poziomu określone jako maszyny o skończonych stanach.
- Sieci komunikujących się automatów, tj. maszyny o skończonych stanach działające równolegle i zsynchronizowane (za pomocą operatorów algebry procesów lub wektorów synchronizacji).
Kilka narzędzi do sprawdzania równoważności (minimalizacja i porównania relacji modulo bisymulacji), takich jak BCG_MIN i BISIMULATOR.
Kilka programów do sprawdzania modeli dla różnych logiki temporalnej i rachunku różniczkowego, takich jak EVALUATOR i XTL.
Połączenie kilku algorytmów weryfikacji: weryfikacja wyliczeniowa, weryfikacja w locie, weryfikacja symboliczna przy użyciu binarnych diagramów decyzyjnych, minimalizacja składu, rzędy częściowe, sprawdzanie modelu rozproszonego itp.
Plus inne narzędzia z zaawansowanymi funkcjami, takimi jak kontrola wizualna, ocena wydajności itp.

CADP jest zaprojektowany w sposób modułowy i kładzie nacisk na pośrednie formaty i interfejsy programistyczne (takie jak środowiska oprogramowania BCG i OPEN/CAESAR), które pozwalają łączyć narzędzia CADP z innymi narzędziami i dostosowywać je do różnych języków specyfikacji.

Modele i techniki weryfikacji

Weryfikacja to porównanie złożonego systemu ze zbiorem właściwości charakteryzujących zamierzone funkcjonowanie systemu (np. wolność od impasu, wzajemne wykluczanie, sprawiedliwość itp.).

Większość algorytmów weryfikacji w CADP opiera się na modelu oznaczonych systemów przejściowych (lub po prostu automatów lub grafów), który składa się ze zbioru stanów, stanu początkowego i relacji przejścia między stanami. Model ten jest często generowany automatycznie na podstawie opisów wysokiego poziomu badanego systemu, a następnie porównywany z właściwościami systemu przy użyciu różnych procedur decyzyjnych. W zależności od formalizmu użytego do wyrażenia właściwości możliwe są dwa podejścia:

Właściwości behawioralne wyrażają zamierzone funkcjonowanie systemu w postaci automatów (lub opisów wyższego poziomu, które są następnie tłumaczone na automaty). W takim przypadku naturalnym podejściem do weryfikacji jest sprawdzanie równoważności , które polega na porównaniu modelu systemu i jego właściwości (obie reprezentowane jako automaty) modulo pewnej równoważności lub relacji preorder. CADP zawiera narzędzia do sprawdzania równoważności, które porównują i minimalizują automaty modulo różne relacje równoważności i preorderów; niektóre z tych narzędzi mają również zastosowanie do modeli stochastycznych i probabilistycznych (takich jak łańcuchy Markowa). CADP zawiera również narzędzia do kontroli wizualnej, których można użyć do weryfikacji graficznej reprezentacji systemu.
Własności logiczne wyrażają zamierzone funkcjonowanie systemu w postaci czasowych formuł logicznych. W takim przypadku naturalnym podejściem do weryfikacji jest sprawdzanie modelu , które polega na rozstrzygnięciu, czy model systemu spełnia właściwości logiczne. CADP zawiera narzędzia do sprawdzania modeli dla potężnej formy logiki temporalnej, rachunku modalnego mu-calculus, który jest rozszerzony o wpisane zmienne i wyrażenia, aby wyrazić predykaty dotyczące danych zawartych w modelu. To rozszerzenie zapewnia właściwości, których nie można wyrazić w standardowym rachunku różniczkowym (na przykład fakt, że wartość danej zmiennej zawsze rośnie wzdłuż dowolnej ścieżki wykonania).

Chociaż techniki te są wydajne i zautomatyzowane, ich głównym ograniczeniem jest problem eksplozji stanów, który pojawia się, gdy modele są zbyt duże, aby zmieściły się w pamięci komputera. CADP zapewnia technologie oprogramowania do obsługi modeli na dwa uzupełniające się sposoby:

Małe modele można przedstawić jawnie, przechowując w pamięci wszystkie ich stany i przejścia (wyczerpująca weryfikacja);
Większe modele są reprezentowane niejawnie, poprzez badanie tylko stanów i przejść modelu potrzebnych do weryfikacji (weryfikacja w locie).

Języki i techniki kompilacji

Dokładna specyfikacja niezawodnych, złożonych systemów wymaga języka, który jest wykonywalny (do weryfikacji enumeratywnej) i ma formalną semantykę (aby uniknąć wszelkich dwuznaczności językowych, które mogłyby prowadzić do rozbieżności interpretacyjnych między projektantami a wykonawcami). Semantyka formalna jest wymagana również wtedy, gdy konieczne jest ustalenie poprawności systemu nieskończonego; nie można tego zrobić za pomocą technik wyliczeniowych, ponieważ zajmują się one tylko skończonymi abstrakcjami, więc należy to zrobić za pomocą technik dowodzenia twierdzeń, które mają zastosowanie tylko do języków z semantyką formalną.

CADP działa na LOTOS- owym opisie systemu. LOTOS to międzynarodowy standard opisu protokołów (norma ISO/IEC 8807:1989), który łączy koncepcje algebr procesów (w szczególności CCS i CSP oraz algebraicznych abstrakcyjnych typów danych. Dzięki temu LOTOS może opisywać zarówno asynchroniczne procesy współbieżne, jak i złożone struktury danych .

LOTOS został mocno zrewidowany w 2001 roku, co doprowadziło do publikacji E-LOTOS (Enhanced-Lotos, norma ISO/IEC 15437:2001), który stara się zapewnić większą wyrazistość (np. ograniczenia czasowe) wraz z większą przyjaznością dla użytkownika.

Istnieje kilka narzędzi do konwersji opisów w innych obliczeniach procesowych lub formatach pośrednich na LOTOS, dzięki czemu narzędzia CADP mogą być następnie wykorzystane do weryfikacji.

Licencjonowanie i instalacja

CADP jest dystrybuowany bezpłatnie do uniwersytetów i publicznych ośrodków badawczych. Użytkownicy w przemyśle mogą uzyskać licencję ewaluacyjną do użytku niekomercyjnego przez ograniczony czas, po upływie którego wymagana jest pełna licencja. Aby poprosić o kopię CADP, wypełnij formularz rejestracyjny pod adresem. Po podpisaniu umowy licencyjnej otrzymasz szczegółowe informacje o tym, jak pobrać i zainstalować CADP.

Podsumowanie narzędzi

Zestaw narzędzi zawiera kilka narzędzi:

CAESAR.ADT to kompilator, który tłumaczy abstrakcyjne typy danych LOTOS na typy C i funkcje C. Tłumaczenie obejmuje techniki kompilacji polegające na dopasowywaniu wzorców i automatyczne rozpoznawanie typowych typów (liczby całkowite, wyliczenia, krotki itp.), które są optymalnie implementowane.
CAESAR to kompilator, który tłumaczy procesy LOTOS na kod C (do szybkiego prototypowania i testowania) lub grafy skończone (do weryfikacji). Tłumaczenie odbywa się za pomocą kilku etapów pośrednich, między innymi konstrukcji sieci Petriego rozszerzonej o wpisane zmienne, funkcje obsługi danych i przejścia atomowe.
OPEN/CAESAR to ogólne środowisko oprogramowania do tworzenia narzędzi eksplorujących wykresy w locie (na przykład narzędzia do symulacji, weryfikacji i generowania testów). Takie narzędzia można rozwijać niezależnie od konkretnego języka wysokiego poziomu. Pod tym względem OPEN/CAESAR odgrywa centralną rolę w CADP, łącząc narzędzia zorientowane językowo z narzędziami zorientowanymi na model. OPEN/CAESAR składa się z zestawu 16 bibliotek kodu wraz z ich interfejsami programistycznymi, takimi jak:
- Caesar_Hash, który zawiera kilka funkcji skrótu
- Caesar_Solve, który rozwiązuje układy równań boolowskich w locie
- Caesar_Stack, który implementuje stosy do eksploracji wyszukiwania w głąb
- Caesar_Table, który obsługuje tablice stanów, przejść, etykiet itp.

W środowisku OPEN/CAESAR opracowano szereg narzędzi:

- BISIMULATOR, który sprawdza równoważności bisymulacji i preorderów
- CUNCTATOR, który przeprowadza symulację stanu ustalonego w locie
- DETERMINATOR, który eliminuje stochastyczny niedeterminizm w układach normalnych, probabilistycznych lub stochastycznych
- DISTRIBUTOR, który generuje wykres stanów osiągalnych za pomocą kilku maszyn
- EWALUATOR, który ocenia regularne formuły mu-rachunku bez zmian
- EXECUTOR, który wykonuje losowe wykonanie kodu
- WYSTAWCA, który wyszukuje sekwencje wykonania pasujące do podanego wyrażenia regularnego
- GENERATOR, który konstruuje wykres stanów osiągalnych
- PREDYKTOR, który przewiduje wykonalność analizy osiągalności,
- PROJEKTOR, który oblicza abstrakcje komunikujących się systemów
- REDUKTOR, który konstruuje i minimalizuje wykres stanów osiągalnych modulo różnych relacji równoważności
- SIMULATOR, X-SIMULATOR i OCIS, które umożliwiają interaktywną symulację
- TERMINATOR, który wyszukuje stany zakleszczenia
BCG (Binary Coded Graphs) to zarówno format pliku do przechowywania bardzo dużych wykresów na dysku (przy użyciu wydajnych technik kompresji), jak i środowisko oprogramowania do obsługi tego formatu, w tym partycjonowanie wykresów do przetwarzania rozproszonego. BCG odgrywa również kluczową rolę w CADP, ponieważ wiele narzędzi opiera się na tym formacie dla swoich danych wejściowych/wyjściowych. Środowisko BCG składa się z różnych bibliotek z ich interfejsami programistycznymi oraz kilku narzędzi, w tym:
- BCG_DRAW, który buduje dwuwymiarowy widok wykresu,
- BCG_EDIT, który umożliwia interaktywną modyfikację układu wykresu utworzonego przez Bcg_Draw
- BCG_GRAPH, który generuje różne formy praktycznie użytecznych wykresów
- BCG_INFO, który wyświetla różne informacje statystyczne dotyczące wykresu
- BCG_IO, który wykonuje konwersje między BCG a wieloma innymi formatami wykresów
- BCG_LABELS, który ukrywa i/lub zmienia nazwy (za pomocą wyrażeń regularnych) etykiet przejścia wykresu
- BCG_MERGE, który gromadzi fragmenty grafu uzyskane z konstrukcji grafu rozproszonego
- BCG_MIN, który minimalizuje grafy modulo silne lub rozgałęzione równoważności (a także radzi sobie z systemami probabilistycznymi i stochastycznymi)
- BCG_STEADY, który przeprowadza analizę numeryczną w stanie ustalonym (rozszerzonych) łańcuchów Markowa w czasie ciągłym
- BCG_TRANSIENT, który przeprowadza przejściową analizę numeryczną (rozszerzonych) łańcuchów Markowa w czasie ciągłym
- PBG_CP, który kopiuje podzielony na partycje wykres BCG
- PBG_INFO, które wyświetla informacje o podzielonym grafie BCG
- PBG_MV, który przenosi podzielony na partycje wykres BCG
- PBG_RM, który usuwa podzielony na partycje wykres BCG
- XTL (eXecutable Temporal Language), który jest funkcjonalnym językiem wysokiego poziomu do programowania algorytmów eksploracji na grafach BCG. XTL zapewnia prymitywy do obsługi stanów, przejść, etykiet, następników i poprzedników funkcji itp. Na przykład można zdefiniować funkcje rekurencyjne na zbiorach stanów, które pozwalają określić w ocenie XTL i generowaniu diagnostyki algorytmy punktów stałych dla zwykłych logik czasowych (takich jak jak HML, CTL, ACTL itp.).

Połączenie między modelami jawnymi (takimi jak grafy BCG) i modelami niejawnymi (eksplorowanymi w locie) zapewniają kompilatory zgodne z OPEN/CAESAR, w tym:

- CAESAR.OPEN, dla modeli wyrażonych jako opisy LOTOS
- BCG.OPEN, dla modeli reprezentowanych jako wykresy BCG
- EXP.OPEN, dla modeli wyrażonych jako automaty komunikujące się
- FSP.OPEN, dla modeli wyrażonych jako opisy FSP
- LNT.OPEN, dla modeli wyrażonych jako opisy LNT
- SEQ.OPEN, dla modeli reprezentowanych jako zestawy śladów wykonania

Zestaw narzędzi CADP zawiera również dodatkowe narzędzia, takie jak ALDEBARAN i TGV (Test Generation based on Verification) opracowane przez laboratorium Verimag (Grenoble) i zespół projektowy Vertecs z INRIA Rennes.

Narzędzia CADP są dobrze zintegrowane i łatwo dostępne za pomocą interfejsu graficznego EUCALYPTUS lub języka skryptowego SVL. Zarówno EUCALYPTUS, jak i SVL zapewniają użytkownikom łatwy, jednolity dostęp do narzędzi CADP, automatycznie dokonując konwersji formatu plików w razie potrzeby i dostarczając odpowiednie opcje wiersza poleceń podczas wywoływania narzędzi.

Nagrody

W 2002 roku Radu Mateescu, który zaprojektował i rozwinął sprawdzanie modeli CADP EVALUATOR, otrzymał Nagrodę Informatyczną przyznawaną podczas 10. edycji dorocznego sympozjum organizowanego przez Fundację Rhône-Alpes Futur.

W 2011 roku Hubert Garavel, architekt oprogramowania i programista CADP, otrzymał nagrodę Gay-Lussaca Humboldta .

W 2019 roku Frédéric Lang i Franco Mazzanti zdobyli wszystkie złote medale za równoległe problemy wyzwania RERS, używając CADP do pomyślnej i prawidłowej oceny 360 formuł obliczeniowej logiki drzewa (CTL) i liniowej logiki czasowej (LTL) na różnych zestawach komunikujących się stanów maszyny.

W 2020 roku Frédéric Lang, Franco Mazzanti i Wendelin Serwe zdobyli trzy złote medale w wyzwaniu RERS'2020, poprawnie rozwiązując 88% problemów „Parallel CTL”, udzielając odpowiedzi „nie wiem” tylko dla 11 formuł z 90 W 2021 r .

Hubert Garavel, Frédéric Lang, Radu Mateescu i Wendelin Serwe wspólnie zdobyli Nagrodę Innowacji Inria – Académie des sciences – Dassault Systèmes za pracę naukową, która doprowadziła do opracowania zestawu narzędzi CADP.

Zobacz też

SYNTAX (używany do budowy wielu kompilatorów i tłumaczy CADP )

Linki zewnętrzne