Időzített rendszerek és az UPPAAL II
Dr. Németh L. Zoltán (
[email protected]) SZTE, Informatikai Tanszékcsoport 2008/2009 I. félév
2008.11.15
MODELL 11
1
Rendszerek leírása az UPPAAL-ban • Modellelenőrzés = modell + specifikációk • a specifikációk megadását, már láttuk – időzített CTL formulák (megszorításokkal): A[ ] P, A<>P, E[ ]P, E<> P, P --> Q
• a modell megadásához kiterjesztett időzített automata hálózatokat használunk – időzített: valós idejű órák, melyek újraindíthatók és tesztelhetők – kiterjesztett: korlátos egész változókat is használhatunk – hálózat: az automaták, a csatornák szerint szinkronizálnak: egy üzenet? átmenet csak egy másik automata üzenet! átmenetével egyszerre hajtható végre 2008.11.14
MODELL 11
2
A modell leírásának részei: • globális és lokális deklarációk – – – – –
konstansok változók csatornák órák tömbök, rekordok, skalárok, metaváltozók, felhasználói típusok
• automata sablonok (automata templates) – ezek az egyes folyamatok modelljei – ide tartoznak a lokális deklarációk
• rendszer komponenseinek megadása (system definition) – a rendszer felépítése a sablonok folyamatokká példányosítsásaival,pl: ember1:=embertipus(1000); ember2:=embertipus(2000); lampa4.xml system lampa,ember1,ember2; 2008.11.14
MODELL 11
3
Típusok, változó, konstansok, tömbök • Az UPPAAL deklarációi a C nyelvhez hasonlóak: Type ::= Prefix TypeId Prefix ::= 'urgent'|'broadcast'|'meta'|'const' TypeId ::= ID|'int'|'clock'|'chan'|'bool'| 'int''['Expression','Expression'']'| 'scalar''['Expression']'| 'struct''{'FieldDecl(FieldDecl)*'}' FieldDecl ::= Type ID ArrayDecl* (','ID ArrayDecl*)*';‘ ArrayDecl ::= '['Expression']'|'[' Type ']' • Expression szintén a C-hez hasonló kifejezés, ld. a HELPben 2008.11.14
MODELL 11
4
Példák I • const int a = 1; a egész típusú konstans, kezdeti értéke 1, az egészek alapértelmezett értékkészlete [-32768, 32767] • bool b[8], c[4]; b és c két 8 illetve 4 elemű tömb, melyek Boole értékeket tartalmaznak Nem keverendő!
• int[0,100] a=5;
a egy korlátozott egész, értéke 1 és 100 közötti lehet, kezdetben 5
kétdimenziós egész értékeket • int a[2][3]= {{1,2,3},{4,5,6}};tartalmazó tömb, kezdeti értékadással
2008.11.14
MODELL 11
5
Példák II • clock x, y; • chan d;
x és y két óra d egy csatorna avagy tevékenység neve, d? és d! használható a szinkronizáláshoz
• urgent chan e;
e egy sürgős (urgent) csatorna, ha az üzenet küldés-fogadás létrejöhet nem választhatunk helyette szünet átmenetet
• struct{int a;bool b;} s1={2,true}; s1 egy olyan rekord, melynek a komponense egész (kezdetben 2), második komponense Boole típusú (kezdetben igaz). • meta int swap; metaváltozó, a modell állapotait nem növeli int a; int b; assign swap=a; a=b; b=swap;
2008.11.14
MODELL 11
6
Kiterjesztett időzített automaták 2.szinkronizálás
invariánsok
3.értékadások
1.őrfeltételek
2008.11.14
MODELL 11
7
1. Őrfeltételek • Boole értékre értéklődjenek ki • csak óra változókra, egészekre és konstansokra (valamint azok tömbjeinek elemeire) hivatkozhatunk • az operandusok megfelelő típusúak kell, hogy legyenek kivéve az int – bool konverziót • óra változók, és azok különbsége csak egészekkel hasonlítható össze (ezért az órákat egész értékűeknek gondolhatjuk) • mellékhatás mentesek (side-effect free) kell hogy legyenek • különböző órákra vonatkozó feltételeket csak konjunkvióval köthetünk össze • diszjunkcióval nem, pl: x <100 or y==50 tilos 2008.11.14
MODELL 11
8
2. Szinkronizációk I • a csatornákat (avagy cselekvések (actions) neveit) globálisan kell deklariálni • lokális csatornáknak nincs értelme, mert nem látja a másik automata, amivel szinkronizálni akarunk • szabad belőlük tömböt szervezni, • azaz egész értékekkel paraméterezni • pl. chan csat[3] • ekkor csat[2]! alatt gondolhatjuk azt, hogy 2-t küldjük el a csat csatornába • de gondolhatjuk azt is, hogy 3 különböző cselekvéssel tudunk szinkronizálni csat[0], csat[1], csat[2] • a sürgős (urgent) csatornákról később lesz szó
2008.11.14
MODELL 11
9
2. Szinkronizációk II Bináris szinkronizáció • két folyamat (automata) között • egy küldő – egy fogadó fél • Példa: • chan a, b[3]; küldés: c[t]! (ha t értéke 2) fogadás: c[2]? • Csak akkor hajtható végre, ha van fogadó fél különben blokkol.
Brodcast szinkronizáció • több folyamat (automa között) • egy küldő – teszőleges számú (esetleg nulla!) fogadó fél • Pl: broadcast chan a; küldés: a! fogadás: a? • minden végrehajtható a? átmenettel rendelkező automatának szinkronizálni kell a küldővel • küldeni mindig lehet • a! soha sem blokkol ebreszto.xml
2008.11.14
MODELL 11
10
3. értékadások • az átmenet sorrendben harmadik lépései, megváltoztatják a modell állapotát • az őrfeltételekkel szemben itt éppen a mellékhatás a lényeg • a típusokat itt is egyeztetni kell • itt is csak konstansa, órára, egész változóra (és ezek tömbjeire) hivatkozhatunk • az óra változóknak csak egész érték adható
2008.11.14
MODELL 11
11
Invariánsok • az állapotokhoz és nem az átmenetkhez kapcsolódnak • Boole értékre értékelődnek ki • mellékhatás mentesek • (x < e) és (x <= e) alakú feltételek konjunkciói – ahol x óraváltozó – e pedig egész értékű kifejezés
2008.11.14
MODELL 11
12
Sablonok (Templates) • kényelmes módszer több azonos, vagy hasonló folyamat definiálására • mint a SPIN-ben a proctype • az automata sablonokat korlátozott egész értékű paraméterekkel láthatjuk el • a sablon neve utáni Parameters mezőben kell megadni őket a változó deklarációhoz hasonlóan • a rendszerdeklarációkban példányosíthatjuk őket a konkrét paraméterek megadásával (ekkor érték szerinti paraméterátadás történik) • vagy ha nem adjuk meg a paramétereket az UPPAAL önműködően létrehozza a példányokat a paramétereket az összes lehetséges módom megválasztva • Példák régebbről:
lampa4.xml, ebreszto.xml
2008.11.14
MODELL 11
13
Sürgősség és elkötelezettség (Urgency and commotment) • • • •
a modellezéshez sokszor szükségünk van arra, hogy a rendszer ne várkozhasson bizonyos állapotokban hanem haladás (progress) történjen, például egy szinkronizáció azonnal létrejöjjön, mihelyt mindkét fél készen áll az erre szolgálló eszközök: • • •
•
sürgős csatornák (urgent channels) sürgős helyek (urgent locations) elkötelezett helyek (committed locations)
ezek az eszközök jelentősen csökkenthetik a szükséges órák számát és az állapottér méretét is 2008.11.14
MODELL 11
14
Sürgős csatornák, sürgős helyek, elkötelezett helyek 1.
sürgős csatornák (urgent channels) – – – – –
2.
sürgős helyek (urgent locations) – –
3.
ha a csatornán keresztül szinkronizálni lehet sem a küldő sem a fogadó nem tehet szünet átmenetet de egymást persze meg kell várniuk órákra vonatkozó őrfeltétel nem lehet a szinkronizáló átmeneten de egészekre vonatkozó őrfeltétel igen deklarációja urgent chan a, b[12]; ezen a helyen nem telhet az idő de a többi folyamat diszkrét átmeneteket tehet közben (azok alatt nem telik az idő)
elkötelezett helyek (committed locations) – – –
ezen a helyen sem telhet az idő, sőt a következő átmenetnek innen, vagy legalább egy másik elkötelezett helyről kell indulnia azaz a többi folyamat normál állapotaival szemben elsőbbséget élvez surgos.xml
2008.11.14
MODELL 11
15
További lehetőségek • •
Néhány további eszköz mely hasznos lehet a modellezéshez: választások (select statements) – –
• •
felhasználói típusok, és rekordok (mint a C-ben.) forall / exists kifejezések – –
•
forall (x:int[0,50]) expr exists (x:int[0,50]) expr
skalárok – – –
•
select = nemtereminisztikus választás az átmenet ,,előtt” pl. k : int[1,6] egy 1 és 6 közötti számot választ
scalar[3] d, a skalárok csak értékadásra és egyenlőség tesztelésére használatos így köztük nincs < >rendezés így a szimmetriájuk kihasználható az állapoptszám csökkentésére
metaváltozók –
meta int swap
2008.11.14
MODELL 11
16
Gyakorlat Egy LEGO kocka válogató UPPAAL modllje • LEGO kocka válogató (brick sorter) • valami hasonló, mint: http://www.norgesgade14.dk/bricksorter.php • elemezzük a modellt: • további példák: www.cs.aau.dk/~kgl/ESV04/exercises/index.html • könnyű HF zuhanyos példa (18) boxes.xml
2008.11.14
MODELL 11
17
