Időzített rendszerek és az UPPAAL
Dr. Németh L. Zoltán (
[email protected]) SZTE, Informatikai Tanszékcsoport 2008/2009 I. félév
2008.11.14
MODELL 10
1
Időzített rendszerek • Real Time Systems = valós idejű rendszerek • Olyan rendszerek, melyek helyessége, nem csak a folyamatok lépéseinek logikai sorrendjétől, de a lépések megtételének idejétől is függ. A rendszernek időbeli korlátozásokat is teljesítenie kell. • Mindenütt jelen vannak, például: – – – – – –
valós idejű operációs rendszerek valós idejű protokollok autóelektronika (ABS, légzsákok, Cruise Control/Tempomat ) szórakoztató elektronika robotok, ipari gépek, gyártósorok közlekedés (lámpák, légi irányítás, űrhajózás, stb.)
• általánosan RT rendszereket vezérlő hardverek / szoftverek – bemenet: szenzorok (érzékelők, sensors) – kimenet: aktuátorok (cselekvők, actuators) 2008.11.14
MODELL 10
2
Egy egyszerű példa • Két fokozatú villanykapcsoló • A rendszer állapotai: – KI: a lámpa nem világít – HALVÁNY: hangulatvilágítás, kis fényerő – VILÁGOS: erős fény
• A felhasználó (most ő lesz a rendszer környezete)egyetlen gomb megnyomásával vezérelhesse a rendszert: – gombnyomás vagy csak gomb
2008.11.14
MODELL 10
3
Időzítés nélkül gombnyomás?
KI
2008.11.14
gombnyomás?
KIS FÉNY
MODELL 10
gombnyomás?
VILÁGOS
4
Időzített automatával gomb?
gomb? x:=0 KI
KIS FÉNY
gomb? x≤500
VILÁGOS
gomb? x>500
• • • • •
ahol x egy valsó idejű óra mondjuk miliszekundomokban (500 = fél másodperc) a zölddel írtak őrfeltételek (csak ekkor hajtható végre az átmenet) a pirossal írt x:=0 az óra újraindítása (reset) azaz két gyors (<500ms) gombnyomás kell a VILÁGOS-ra állításhoz 2008.11.14
MODELL 10
5
Időzített automaták átmenetei I p x≥30 & y=10 a x:=0 q
2008.11.14
őrfeltételek: órák egésszekkel vett összehasonlításainak (<, ≤, =, ≥, >) Boole kombinációi tevékenység (action) ezekkel lehet szinkronizálni óra újraindítások (resets)
MODELL 10
6
Időzített automaták átmenetei II Állapotok p
(hely, x=u, y=v) hármasok, ahol x≥30 & y=10 a x:=0
– hely ∈ { p, q } – u, v valós számok
Átmenetek • diszkrét átmentek: (p,x=12.5,y=3.14)a––> (q,x=0,y=3.14)
q
• szünet átmenetek: e(1.1)
(p,x=12.5,y=3.14) ––> (p,x=13.6,y=4.24)
2008.11.14
MODELL 10
7
Egy lehetséges futás gomb?
gomb? x:=0 KI
2008.11.14
VILÁGOS
gomb? x>500
átmenet: e(200) gomb? e(350) gomb?
KIS FÉNY
gomb? x≤500
⇒ ⇒ ⇒ ⇒
állapot: (KI, x=0 ) (KI, x=200) (KIS FÉNY, x=0) (KIS FÉNY, x=350) (VILÁGOS, x=350) MODELL 10
8
Magától kikapcsoló lámpa x:=0 x=60000
KI
gomb? x:=0
KISFÉNY
gomb? x≤500 x:=0
x≤60000
x:=0
VILÁGOS x≤60000
gomb? x:=0
gomb? x:=0
x:=0 x=60000
• a kék x≤60000 feltételek invariánsok (előrehaladást tudunk velük kifejezni) • a rendszer futásának az állapotra vonatkozó invariánsokat teljesíteni kell • azaz sem KISFÉNY sem VILÁGOS állapotban nem várhatunk tovább 1 percnél • egy perc után, ha újabb gombnyomás nem érkezik, a lámpa kikapcsol • így pl. (KISFÉNY,x=0) ---e(65000)Æ nem lehetséges 2008.11.14
MODELL 10
9
A lámpa UPPAAL modelljei gyakorlat I • lampa1.xml: – az időzítés nélküli modell, – hogy kell definiálni állapotokat, átmeneteket – hogyan működik a szimuláció, mit jelent a szinkronizálás
• lampa2.xml: – – – –
az időzítés bevezetésével kapott modell felépítése őrfeltételek óra újraindítások szimulációk
• lampa3.xml: – az egy perc után magától kikapcsoló lámpa modellje – invariánsok használata – verifikáció 2008.11.14
MODELL 10
10
Specifikációi az UPPAAL-ban • A CTL (Computation Tree Logic) megszorított változata használható, a jelölés egy kicsit más: A = Allways /minden futásnál/ [ ] = Globally /minden állapotban/
E = there Exists /van olyan futás/ <> = Future /valamelyik állapotban/
• Így a CTL jelölésével: A[ ] = AG, A<> = AF, E[ ] = EG, E<> = EF • És még bounded livness (időben korlátozott élőségi) tulajdonságok is • Bonyolultabb tulajdonságok egy monitor folyamat felvételével ellenőrizhetők • Mind a diszkrét, mind a szünet átmeneteket figyelembe kell venni
2008.11.14
MODELL 10
11
Specifikáció az UPPAAL-ban II • Possibility (lehetségesség) E<> P : van olyan futás mely során valamikor igaz lesz P • Safety (biztonsági tulajdonságok) – –
invariáns: A[ ] P : minden futás minden állapotában igaz P lehetséges invariáns: E[ ] P van olyan futás, melynek minden igaz P
állapotában
• Liveness (élőségi tulajdonságok) – végül is: A<> P : minden úton valamikor P teljesül – válasz: P -> Q : minden úton, ha P teljesül, akkor valamikor Q is teljesülni fog
• Bounded liveness (korlátos élőségi) – válasz időn belül: P ->≤t Q : minden úton, ha P teljesül, akkor valamikor Q is teljesülni fog t időn belül. 2008.11.14
MODELL 10
12
Specifikáció az UPPAAL-ban III • Az előzőekben P és Q olyan kifejezések melyek – hivatkozhatbak: • • • •
egész változókra konstansokra óra változók értékeire folyamatok aktuális állapotaira
– bennük a típusok megfelelőek – a kifejezés mellékhatás mentes és – Boole értékre értékelődik ki
• így pl. a szokásos Boole-műveletek használhatók: • not • or, and • imply (a jelenben nem keverendő a ->-lal, mely időbeli választ jelent) 2008.11.14
MODELL 10
13
Néhány egyszerű azonosság • • • • •
not A [ ] P = E <> not P not A <> P = E [ ] not P P -> Q = A [ ] ( P imply A <> Q ) Ez utóbbi tehát CTL-ben is kifejezhető De a CTL-lel szemben az UPPAAL nem engedi meg az időoperátorok egymásba ágyazását • pl: A[ ] ( E <> P ) nem írható
2008.11.14
MODELL 10
14
A lámpa UPPAAL modelljei gyakorlat II • lampa3.q: – CTL formulák megadása – a specifikációk ellenőrzése – a hiba trace elemzése a szimulátorban
• lampa4.xml: – sablonok (templates) használata, paraméterezés – a rendszer deklarációja – további tulajdonságok elenőrzése
2008.11.14
MODELL 10
15
