Powi ˛azane formalizmy

Alvis Editor

diagram komunikacji + warstwa kodu

Alvis Compiler

Alvis → Posta´c po´srednia w Haskell

Dowolny edytor tekstu doł ˛aczenie własnego kodu Haskell

Kompilator GHC plik XML plik Haskell plik Haskell plik Haskell (0) A: (X,1,[],()) B: (X,1,[],()) (1) A: (X,2,[],()) B: (X,1,[],()) loop(A) (2) A: (X,1,[],()) B: (X,2,[],()) loop(B) (3) A: (W,2,[out(a)],()) B: (X,1,[],()) out(A.a) (4) A: (X,2,[],()) B: (X,2,[],()) loop(B) loop(A) (5) A: (X,1,[],()) B: (W,2,[in(b)],()) in(B.b) (6) A: (W,2,[out(a)],()) B: (X,2,[],()) loop(B) out(A.a) (7) A: (X,2,[],()) B: (W,2,[in(b)],()) in(B.b) loop(A) in(B.b) out(A.a) plik DOT 0 1 loop(A) 2 loop(B) 3 out(A.a) 4 loop(B) loop(A) 5 in(B.b) 6 loop(B)out(A.a) 7 in(B.b) loop(A) in(B.b) out(A.a) plik Aldebaran 0; A; X; 1; []; (); B; X; 1; ... 1; A; X; 2; []; (); B; X; 1; ... 2; A; X; 1; []; (); B; X; 2; ... 3; A; W; 2; [out(a)]; (); B; ... 4; A; X; 2; []; (); B; X; 2; ... 5; A; X; 1; []; (); B; W; 2; ... 6; A; W; 2; [out(a)]; (); B; ... 7; A; X; 2; []; (); B; W; 2; ... plik TXT

?

wykonanie pliku binarnego (mo˙zliwe wyniki)

Rysunek 2.6: Proces modelowania i weryfikacji przy wykorzystaniu j˛ezyka Alvis. znajduje si˛e w rozdziale 5.

Wi˛ecej informacji na temat narz˛edzi wspieraj ˛acych wykorzystanie j˛ezyka Alvis jest dost˛epnych w in-strukcji znajduj ˛acej si˛e na stronie projektu [113].

2.6 Powi ˛azane formalizmy

W niniejszym podrozdziale zawarto opis wybranych popularnych formalnych j˛ezyków modelowania, które mog ˛aby´c u˙zywane podobnie jak Alvis do modelowania i weryfikacji dyskretnych systemów współbie˙znych czasowych i/lub nieczasowych.

2.6. Powi ˛azane formalizmy 21

2.6.1 Sieci Petriego

Sieci Petriego s ˛a niew ˛atpliwie najbardziej popularn ˛a grup ˛a formalnych j˛ezyków modelowania. Słu˙z ˛a do formalnego, graficznego opisu i analizy systemów współbie˙znych. Od ich wprowadzenia w latach 60. przez Carla A. Petriego [95] zostało zaproponowanych przynajmniej kilkadziesi ˛at wariantów (klas) sieci b˛ed ˛acych rozwini˛eciem oryginalnej koncepcji, dzi˛eki czemu u˙zytkownik ma mo˙zliwo´s´c dobrania odpowiedniej klasy do modelowanego problemu. Podstawow ˛aró˙znic ˛apomi˛edzy sieciami Petriego, a j˛ezykiem Alvis jest wysoki próg wej´scia w ten formalizm. Stworzenie nawet prostego modelu wymaga od u˙zytkownika długotrwałego treningu. Dodatkowo, dla skomplikowanych systemów sieci Petriego s ˛a bardzo szybko si˛e rozrastaj ˛a, sta-j ˛ac si˛e ci˛e˙zkimi do zrozumienia nawet dla do´swiadczonych in˙zynierów. Nasta-jprawdopodobniesta-j nasta-jbli˙zsz ˛a Alvisowi klas ˛a s ˛a kolorowane czasowe sieci Petriego (Timed coloured Petri nets [68]). Pozwalaj ˛a one na modelowanie zdarze´n dyskretnych ł ˛acz ˛ac mo˙zliwo´sci sieci Petriego z wysokopoziomowym j˛ezykiem pro-gramowania (SML), który umo˙zliwia mi˛edzy innymi definiowanie typów danych, zmiennych, czy wyra˙ze´n do manipulacji danymi [91]. Model czasowy w tej klasie sieci Petriego opiera si˛e na znacznikach czasu, które mog ˛a zosta´c przypisane do tokenów (znaczników), czyli warto´sci przechowywanych w miejscach sieci, podczas odpalania przej´s´c. Poniewa˙z warto´sci znaczników czasowych mog ˛a rosn ˛a´c w niesko´nczo-no´s´c, grafy osi ˛agalno´sci dla tych sieci s ˛a zwykle niesko´nczone. Z tego powodu mo˙zliwo´sci wykorzystania technik weryfikacji modelowej dla modeli stworzonych w kolorowanych czasowych sieciach Petriego s ˛a ograniczone lub wymagaj ˛a generowania alternatywnych sko´nczonych reprezentacji grafów osi ˛agalno´sci np. przez zastosowanie klas równowa˙zno´sci dla stanów i tranzycji. W j˛ezyku Alvis ka˙zde przej´scie mo˙ze mie´c indywidualnie przypisany czas trwania. Poniewa˙z warto´sci nie s ˛a zwi ˛azane z globalnym zegarem, grafy LTS s ˛a zwykle sko´nczone. Kolejn ˛a istotn ˛a ró˙znic ˛a jest to, ˙ze w przypadku sieci kolorowanych reprezentacja graficzna modelu rzadko odzwierciedla struktur˛e modelowanego systemu, utrudniaj ˛ac zarówno proces two-rzenia jak i interpretacji. Diagramy komunikacji w Alvisie znacznie lepiej odzwierciedlaj ˛a rzeczywisto´s´c, poniewa˙z ka˙zdy agent reprezentuje konkretny komponent systemu. Ostatni ˛a wart ˛a wspomnienia ró˙znic ˛a s ˛a mo˙zliwo´sci definiowania własnych typów danych i funkcji manipulacji danymi – Alvis umo˙zliwia to dzi˛eki wykorzystaniu systemu typów Haskella. W przypadku sieci kolorowanych i j˛ezyka SML, dost˛epny jest jedynie ograniczony zbiór typów podstawowych i powi ˛azanych operatorów.

2.6.2 Algebry procesów

Algebry procesów s ˛a drug ˛a popularn ˛a grup ˛a metod formalnych. W ich przypadku opis zachowania systemu wzorowany jest na rachunku algebraicznym – przedstawiaj ˛a zewn˛etrzne zachowania systemu jako ci ˛ag wy-ra˙ze´n algebraicznych. Najbardziej znanymi algebrami procesów s ˛a CCS (Calculus of Communicating Sys-tems, [90], [2]), CSP (Communicating Sequential Processes, [59], [12]) oraz LOTOS [67]. W przypadku algebr procesów proces modelowania opiera si˛e na tworzeniu skryptów opisuj ˛acych dany system. Skrypty

2.6. Powi ˛azane formalizmy 22

mog ˛a mie´c posta´c ci ˛agu równa´n algebraicznych (CCS, CSP) lub kodu (LOTOS). W przypadku CCS i CSP rozwa˙zana jest synchroniczna komunikacja mi˛edzy procesami – procesy wykonuj ˛ace te same akcje s ˛a trak-towane jako komunikuj ˛ace si˛e ze sob ˛a. Podej´scie to, chocia˙z relatywnie proste, niesie ze sob ˛a spore ryzyko niezamierzonego skomunikowania ze sob ˛a ró˙znych cz˛e´sci systemu. Stanowi to bardzo powa˙zny problem, szczególnie w zło˙zonych modelach. W j˛ezyku LOTOS procesy komunikuj ˛a si˛e ze sob ˛a wył ˛acznie synchro-nicznie poprzez tzw. bramy. Stany obiektów definiowane s ˛anatomiast przez abstrakcyjne typy danych. Cho-cia˙z zastosowana notacja przypomina j˛ezyki wysokiego poziomu to bazuje na koncepcjach zapo˙zyczonych z algebr CCS i CSP. Pomimo prób dodania do tego j˛ezyka kompozycji asynchronicznej [82], proces mo-delowania jest ci˛e˙zki do zrozumienia, co skutecznie zniech˛eca in˙zynierów i wstrzymuje jego popularyzacj˛e w in˙zynierii oprogramowania.

Warto wspomnie´c, ˙ze geneza j˛ezyka Alvis jest powi ˛azana z algebrami procesów. J˛ezyk XCCS [7], b˛e-d ˛acy rozszerzeniem algebry CCS o graficzny mob˛e-del poł ˛acze´n mi˛eb˛e-dzy agentami, jest niejako poprzeb˛e-dnikiem Alvisa. Sam Alvis posiada kilka zapo˙zycze´n z algebr procesów, jak cho´cby terminy takie ja agent, port czy kanał komunikacyjny. W przypadku Alvisa jednak wykorzystanie równa´n algebraicznych zostało całkowicie porzucone na rzecz warstwy kodu w j˛ezyku wysokiego poziomu.

2.6.3 Automaty czasowe

Automaty czasowe [11], [4] s ˛a rozszerzeniem automatów sko´nczonych [64] o zmienne zegarowe pozwala-j ˛ace wyrazi´c zale˙zno´sci czasowe w modelu. Zmienne te reprezentupozwala-j ˛a zegary w modelowanym systemie. Ze-gary te s ˛a zerowane podczas startu systemu, a nast˛epnie ich warto´sci synchronicznie wzrastaj ˛a. Dodatkowo, mo˙zna dokona´c niezale˙znego zerowania zegarów i mierzy´c czas jaki upłyn ˛ał od ostatniego wyzerowania. Zegary u˙zywane s ˛ado definiowania warunków czasowych, w których dany system mo˙ze operowa´c, w szcze-gólno´sci do definicji dost˛epnych przej´s´c oraz długo´sci pobytu modelu w danym stanie. W przeciwie´nstwie do j˛ezyka Alvis, nie jest mo˙zliwe zdefiniowanie czasu trwania pojedynczego przej´scia.

Automaty czasowe wykorzystuj ˛a graficzn ˛a reprezentacj˛e systemu oraz umo˙zliwiaj ˛a modularyzacj˛e delu poprzez wprowadzenie hierarchii, jednak opis modelu jest bardzo sformalizowany, a weryfikacja mo-delu wymaga zaawansowanych umiej˛etno´sci matematycznych.

2.6.4 Statechart

Wizualny j˛ezyk modelowania Statechart [56] jest pod wieloma wzgl˛edami podobny do Alvisa. Rozszerza on koncepcj˛e maszyny stanów o trzy kluczowe aspekty: hierarchi˛e, równoległo´s´c i komunikacj˛e. Specyfikacja systemu mo˙ze dzi˛eki temu zosta´c zmodularyzowana. Chocia˙z oryginalna koncepcja nie posiadała modelu czasu, z biegiem lat powstały formalizmy wprowadzaj ˛ace czasowo´s´c. Nale˙z ˛a do nich mi˛edzy innymi Timed Statecharts [69], Real-time Statecharts [50] oraz dwie koncepcje opisane przez twórc˛e j˛ezyka Statechart

2.6. Powi ˛azane formalizmy 23

w jego pó´zniejszej pracy [57].

Najwi˛eksz ˛a przewag ˛a Alvisa nad grup ˛a formalizmów bazuj ˛acych na Statechart jest oddzielenie kodu od warstwy wizualnej, znacznie bardziej zwi˛ezła reprezentacja graficzna oraz mo˙zliwo´s´c dodania dowolnego kodu (dozwolonego w j˛ezyku Haskell) do modelu. Chocia˙z Statechart umo˙zliwia chowanie stanów systemu w kolejnych warstwach, to ostatecznie wszystkie stany systemu musz ˛a znale´z´c swoj ˛a reprezentacj˛e w mo-delu. Warstwa wizualna w j˛ezyku Alvis modeluje jedynie komunikacj˛e, dzi˛eki czemu jest znacznie mniejsza i łatwiejsza do zrozumienia w przypadku modeli rzeczywistych systemów, zawieraj ˛acych miliony stanów. Oddzielenie warstwy kodu pozwala z kolei na reu˙zywalno´s´c (ten sam kod dla wielu agentów) oraz ułatwia zrozumienie modelu przeci˛etnemu programi´scie.

2.6.5 PRISM

PRISM [74] jest probabilistycznym narz˛edziem do formalnego modelowania i analizy modeli stycznych, w tym czasowych ła´ncuchów Markova, procesów decyzyjnych Markova, automatów probabili-stycznych oraz czasowych automatów probabiliprobabili-stycznych [92]. PRISM rozszerza koncepcj˛e maszyny sta-nów o przej´scia probabilistyczne, zmienne zegarowe oraz modularyzacj˛e. Posiada on własny j˛ezyk opisu modelu. Niew ˛atpliw ˛a przewag ˛a PRISM nad Alvisem jest to, ˙ze j˛ezyk ten nie ma problemu z opisywaniem niepewno´sci. W Alvisie istnieje jedynie kilka instrukcji umo˙zliwiaj ˛acych wprowadzenie losowo´sci (instruk-cja pick i komunika(instruk-cja nieblokuj ˛aca). Jednak w przeciwie´nstwie do Alvisa, opis modelu PRISM umo˙zliwia definiowanie zmiennych jedynie kilku typów (boolean i integer z ograniczonym zakresem) oraz wykorzysta-nie wykorzysta-niewielkiej liczby wbudowanych operacji. Innym znanym problemem PRISM jest spore ryzyko popeł-nienia ci˛e˙zkich do znalezienia bł˛edów. Ryzyko to jest zwi ˛azane z tym, ˙ze komunikacja pomi˛edzy modułami mo˙ze by´c zaciemniona przez jawne wywołania zmiennych z innych modułów. Modelowanie w PRISM wy-maga my´slenia na ni˙zszym poziomie abstrakcji – w kategoriach stanów i upływu czasu. U˙zytkownik Alvisa mo˙ze operowa´c na wy˙zszym poziomie, bli˙zszym rzeczywistej implementacji systemu, a przestrze´n stanów jest generowana automatycznie (graf LTS).

Rozdział 3

Intermediate Haskell Representation

Jak zostało przedstawione w rozdziale 2, głównym zadaniem narz˛edzia Alvis Compiler jest translacja mo-delu Alvis do postaci po´sredniej w j˛ezyku funkcyjnym Haskell. Ta po´srednia reprezentacja modeli nazwana została IHR (ang. Intermediate Haskell Representation) [112]. Rozdział ten został po´swi˛econy szerszemu przedstawieniu koncepcji stoj ˛acych za powstaniem postaci po´sredniej oraz opisaniu sposobu reprezentacji stanów i dynamiki modelu w j˛ezyku Haskell.