Prezentowany w niniejszej monografii język Alvis powstał jako wynik poszukiwania języka modelowania, który z jednej strony byłby łatwy do opanowania przez inżyniera informatyka, a z drugiej pozwalał na formalną weryfikację wytworzonego modelu. Język Alvis jest rozwijany w Katedrze Informatyki Stosowanej AGH (Wydział Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej) przez zespół kierowany przez autora.

Kilkunastoletnie doświadczenie autora w stosowaniu metod formalnych, wyrażone m.in. we wcześniejszych monografiach, było podstawą do wyspecyfikowania pożądanych cech budowanego formalizmu, do których zaliczono:

• możliwość formalnej weryfikacji modelu, w szczególności z uwzględnieniem technik weryfikacji modelowej;
• udostępnienie graficznego języka modelowania struktury tworzonego systemu z uwzględnieniem przypływu informacji i sterowania;
• wyposażenie graficznego języka modelowania w konstrukcje umożliwiające hierarchizację modelu i jego rozwijanie przy zastosowaniu zarówno podejścia od ogółu do szczegółu, jak i odwrotnie;
• udostępnienie języka wysokiego poziomu do opisu dynamiki elementów składowych (podsystemów) w modelu;
• możliwość łatwego specyfikowania dynamiki otoczenia w przypadku modelowania systemów wbudowanych;
• ograniczenie elementów języka do niezbędnego minimum.

• Rozdział 1 zawiera wprowadzenie w tematykę pracowania.
• Rozdział 2 jest nieformalnym wprowadzeniem do języka Alvis. Kluczowe elementy języka takie jak diagramy komunikacji, warstwa kodu, komunikacja synchroniczna i asynchroniczna oraz grafy LTS przedstawiono nieformalnie na podstawie przykładowych modeli. Celem tego rozdziału jest wstępne zapoznanie czytelnika z własnościami języka Alvis i jego możliwościami w odniesieniu do modelowania systemów informatycznych.
• Rozdział 3 poświęcono diagramom komunikacji. Stanowią one graficzną warstwę języka Alvis, a ich podstawowym zadaniem jest przedstawienie struktury modelowanego systemu pod względem przepływu danych i sterowania. Diagram komunikacji jest grafem hierarchicznym, co umożliwia konstruowanie bardziej złożonych systemów przy zastosowaniu podsystemów. W rozdziale omówiono diagramy niehierarchiczne, hierarchiczne oraz metody przekształcania diagramów hierarchicznych w szczególności do postaci równoważnych diagramów niehierarchicznych.
• Rozdział 4 dotyczy warstwy kodu języka Alvis. Omówiono w nim instrukcje języka, które są używane do opisu dynamiki poszczególnych agentów. Ponadto warstwa kodu służy do definiowania parametrów agentów, definiowania funkcji operujących na agentach oraz specyfikowania dynamiki otoczenia dla systemów wbudowanych. Stanowi ona połączenie programowania funkcyjnego w języku Haskell z programowaniem imperatywnym opartym na instrukcjach zdefiniowanych dla Alvisa, a wzorowanych m.in. na instrukcjach występujących w języku Ada.
• Rozdział 5 przedstawia semantykę modeli “nieczasowych” z warstwą systemową alfa 0. Modele takie stanowią najbardziej uniwersalną odmianę języka Alvis, przeznaczoną do modelowania systemów współbieżnych. W rozdziale tym formalnie zdefiniowano: model w języku Alvis, stan agenta i stan modelu oraz podano semantykę przejść dla rozważanych modeli. Omówiono również koncepcję grafów etykietowanych przejść, będących grafową reprezentacją przestrzeni stanów osiągalnych dla modelu. Na końcu rozdziału podano przykłady takich grafów.
• Rozdział 6 poświęcono problemowi dołączania do modeli w języku Alvis systemów regułowych. Jest to możliwe po zakodowaniu tablicy decyzyjnej, która reprezentuje zbiór reguł z nieatomicznymi wartościami atrybutów, w postaci funkcji w języku Haskell. Funkcja taka jest używana w warstwie kodu i nie wpływa w żaden sposób na strukturę modelu. Ponadto w rozdziale przedstawiono algorytmy weryfikacji systemów regułowych, zaimplementowane w Haskellu, które pozwalają połączyć proces projektowania systemu regułowego na potrzeby umieszczenia go w modelu w języku Alvis z jego weryfikacją.
• Rozdział 7 opisuje “czasową” wersję języka Alvis z warstwą systemową alfa 0, którą można stosować do modelowania systemów czasu rzeczywistego. Uwzględnienie czasu realizacji poszczególnych kroków pozwala na etapie analizy sprawdzać spełnianie wymagań dotyczących czasu, np. w przypadku modelowania systemów o twardych wymaganiach czasowych. Konsekwencją wprowadzenia czasu jest także zmiana podejścia do generowania etykietowanych systemów przejść (grafów LTS) dla modeli czasowych. Wprowadzone w tym rozdziale SR-grafy z jednej strony redukują liczbę ścieżek w grafie LTS w porównaniu do modeli “nieczasowych”, a z drugiej wymuszają uwzględnianie stanów, które zawierają kroki w trakcie realizacji.
• Rozdział 8 dotyczy metody specyfikacji dynamiki otoczenia dla systemów wbudowanych modelowanych w języku Alvis. Proponowane rozwiązanie pozwala nie tylko znacznie uprościć zarówno etap konstruowania modelu, jak i jego analizy, ale również przyrostowo rozwijać konstruowany model. Podejście to pozwala wstępnie opracować część modelu przy założeniu, że pozostałe jego części są elementami otoczenia, a dopiero po jego weryfikacji rozwijać bardziej szczegółowe jego wersje. Metoda ta umożliwia również określenie zewnętrznych warunków, w jakich chcemy weryfikować model, tzn. odpowiednio wyspecyfikowane sygnały wejściowe generowane przez otoczenie pozwalają na symulację (lub wygenerowanie grafu LTS) dla określonej ścieżki testowej. Z drugiej strony pozwalają one łatwo wprowadzić do modelu elementy losowości w odniesieniu do sygnałów dostarczanych przez otoczenie.
• Rozdział 9 opisuje dwa podejścia do weryfikacji własności modeli w języku Alvis. W pierwszym stosowane jest zewnętrzne narzędzie CADP, które sprawdza, czy model spełnia wymagania zdefiniowane z użyciem logiki modalnej (rachunek μ). Podejście to pozwala wykorzystać techniki weryfikacji modelowej i sprawdzone narzędzia do weryfikacji własności etykietowanych systemów przejść. W drugim podejściu wykorzystano fakt translacji modelu w języku Alvis do kodu źródłowego w Haskellu. Możliwe jest uzupełnienie wygenerowanego kodu własnymi funkcjami, które filtrują listę ze stanami systemu, wyszukując stany lub fragmenty grafu o zadanych własnościach.
• Rozdział 10 zawiera zestawienie ważniejszych rezultatów prac nad językiem Alvis, które przedstawiono w monografii oraz opis perspektywy dalszego rozwoju tego języka.
• Dodatek A przedstawia podstawy programowania w języku Haskell. Przedstawione w nim zagadnienia dotyczą wyłącznie programowania czysto-funkcyjnego. Tematyka dodatku została dobrana tak, by dostarczyć informacje dotyczące Haskella niezbędne ze względu na konstruowanie modeli w Alvisie.
• Dodatek B opisuje oprogramowanie, które jest przydatne przy modelowaniu systemów informatycznych w języku Alvis i które wykorzystano również przy opracowaniu przedstawionych w niniejszej monografii przykładów. Część z opisywanych narzędzi powstało jako prototypowe rozwiązania dedykowane wyłącznie językowi Alvis (Alvis Editor i Alvis Translator), inne stanowią ogólnodostępne narzędzia związane z weryfikacją modelową czy też przetwarzaniem grafów.