Formális módszerek A formális modellezés és a formális verifikáció alapjai dr. Bartha Tamás BME Közlekedés- és Járműirányítási Tanszék
dr. Majzik István Dr. Pataricza András BME Méréstechnika és Információs Rendszerek Tanszék 1
Mire szeretnénk használni a formális módszereket? Milyen problémákkal nézünk szembe? Miben segíthetnek a formális módszerek?
2
Egy tanulságos történet… • Vasa svéd hadihajó, 1628: – Elsüllyedt közvetlenül a vízrebocsátás után
• Problémák: – Változó követelmények (II. Gusztáv Adolf király) – Hiányzó pontos specifikáció (Henrik Hybertsson építő) – Ellenőrizetlen tervek (Johan Isbrandsson alvállalkozó) – Figyelmeztetések figyelmen kívül hagyása (Fleming admirális) •
Irodalom: – –
The Vasa: A Disaster Story with Software Analogies. By Linda Rising. The Software Practitioner, January-February 2001. Why the Vasa Sank: 10 Problems and Some Antidotes for Software Projects. By Richard E. Fairley and Mary Jane Willshire. IEEE Software, March-April 2003. 3
Komplex rendszerek tervezése
- Minimális tervezés - Implicit folyamat - Egyszerű eszközök
- Tervezés - Definiált folyamat - Hatékony eszközök
- Ellenőrzött tervek - Meghatározott folyamat - Automatikus eszközök
4
Szoftver minőségi krízis • Tipikus kódméret: – 10 kLOC … 1000 kLOC
• Fejlesztési ráfordítás: – 0,1 - 0,5 mérnökév / kLOC (nagyméretű szoftver) – 5-10 mérnökév / kLOC (kritikus szoftver)
• Hiba eltávolítás (ellenőrzés, tesztelés, javítás): – 45 - 75% ráfordítás
• Hibasűrűség változása: – 10 - 200 hiba / kLOC jön létre a fejlesztés során Ellenőrzés, debuggolás, javítás – 0,01 - 10 hiba / kLOC maradhat az üzembe helyezésig 5
Alkalmazások fejlesztésének kihívásai • Jó minőségű specifikáció és tervek készítése – Teljes – Ellentmondás-mentes, egyértelmű – Ellenőrizhető
• Tervek ellenőrzése – Tervezői döntések igazolása • Bizonyítottan helyes tervek a továbblépés alapjai
– Hibák elkerülése vagy korai felderítése • Minőség költség fejlesztési idő optimalizálás
• Bizonyított helyességű eszközök használata – Forráskód, konfiguráció, teszt és monitor szintézis
Ezek alapjait a formális módszerek adhatják!
6
Továbblépés: Formális módszerek Formális módszer: • A formális modellről ismeretet adó matematikai eljárás • Eszközökkel támogatható
• A formális modell végrehajtása: Szimuláció • A formális modell ellenőrzése: Formális verifikáció – „Önmagában való” vizsgálat • Konzisztencia, ellentmondás-mentesség • Teljesség, zártság
– „Megfelelés” vizsgálata • Modellek között • Modellek és elvárt tulajdonságok között (implementáció specifikáció)
• A formális modell alapján történő szintézis: – Szoftver (programkód, konfiguráció) generálása – Hardver tervek generálása
7
Verifikáció és validáció összehasonlítása Verifikáció (igazolás)
Validáció (érvényesítés)
„Jól építjük-e a rendszert?”
„Jó rendszert építettünk-e?”
Összhang ellenőrzése a fejlesztési fázisokban, illetve ezek között
A fejlesztés eredményének ellenőrzése
Fejlesztési lépések során használt tervek (modellek) és specifikációjuk közötti megfelelés ellenőrzése
A kész rendszer és a felhasználói elvárások közötti megfelelés ellenőrzése
Objektív folyamat; formalizálható, automatizálható
Szubjektív elvárások lehetnek; elfogadhatósági ellenőrzés
Felderíthető hibák: Tervezési, implementációs hibák
Felderíthető hibák: Követelmények hiányosságai is
Nincs rá szükség, ha automatikus a leképzés követelmény és implementáció között
Nincs rá szükség, ha a specifikáció tökéletes (elég egyszerű) 8
V-től az Y fejlesztési modellig Életciklus
Ráfordítás megtakarítás 0%
Kézi kódolás a V-modell szerint Szoftverfejlesztés “Közönséges” automatikus kódgenerátor használata
Követelmények elemzése
Rendszer specifikálás
-20%
Rendszer validáció
Rendszer verifikáció
Minősített automatikus kódgenerátor használata Architektúra tervezés
-50%
Rendszer integrálás
Modul tervezés
Modul verifikáció
Formális verifikációval kiegészített tervezés
-60%
Modul implementáció
* Adatok: Esterel Technologies
40 50
100%
ráfordítás
9
V-től az Y fejlesztési modellig Életciklus
Ráfordítás megtakarítás 0%
Kézi kódolás “Közönséges” automatikus kódgenerátor használata
-20%
Minősített automatikus kódgenerátor használata
-50%
Formális verifikációval kiegészített tervezés
-60%
* Adatok: Esterel Technologies
40 50
100%
ráfordítás
10
Biztonságkritikus szoftverek fejlesztése • IEC 61508: Szabvány előírások a fejlesztésre – Functional safety in electrical / electronic / programmable electronic safety-related systems – Szakterület-specifikus szabványok alapja
• Követelmény-specifikáció készítésének előírásai:
11
Biztonságkritikus szoftverek fejlesztése • IEC 61508: Szoftver tervezés és fejlesztés előírásai
12
Mik azok a formális módszerek? A formális módszerek célja és eszközei
13
Formális módszerek Matematikai technikák, – elsősorban diszkrét matematika – és matematikai logika
használata arra, hogy elkészítsük és ellenőrizzük hardver és szoftver rendszerek – specifikációját, – terveit (modelljeit),
– implementációját (viselkedését), – dokumentációját. 14
Hogyan ellenőrizhetjük a követelményeket? • A megvalósítás tesztelésével – Létre tudunk-e hozni minden lehetséges végrehajtást lefedő teszt eseteket? – A problémás esetek figyeléséhez külön ellenőrző kell – A hiba már csak az implementáció után derülhet ki, drágán javítható
• Modellezéssel és szimulációval – Tudunk-e szimulálni minden lehetséges végrehajtást? – A problémás esetek detektálása nagy odafigyelést igényel – A hibák viszont olcsóbban javíthatók modell szinten
• Modellezéssel és az állapottér teljes ellenőrzésével – Szisztematikus algoritmus kell az állapottér teljes felvételéhez – Legyen automatikus a követelmények teljesülésének figyelése is • Ehhez egy olyan nyelv szükséges, amikkel a követelmények leírhatók • Általános módszer adható a követelmények modell alapú ellenőrzésére 15
A formális módszerek használata • Tervezők (nem csak matematikusok) által is használható, amennyiben a specifikus tudást eszközökbe integrálják – Modellező eszközök – Ellenőrző eszközök • Modellellenőrzők, ekvivalencia ellenőrzők, automatikus tételbizonyítók
– Szintézis eszközök • Kódgenerátor, konfiguráció generátor az ellenőrzött modellek alapján • Teszt generátor (validáláshoz)
• Csökken a rendszerben maradó koncepcionális és tervezői hibák száma, javul a minőség – Szolgáltatásbiztonság növelhető – De garanciát nem ad a használhatóságra, a felhasználói elvárások teljesítésére! – Validációt nem helyettesíti 16
A formális módszerek használatának lépései •
Valós probléma formális vizsgálata: 1. Fogalmi tér felépítése
feltételezések
2. Probléma formalizálása
absztrakció
3. Formális modell analízise
automatikus lehet
4. Eredmények értelmezése, felhasználása
•
Alkalmazáshoz szükséges: – Feltételezések teljesülésének ellenőrzése – Modell validálása – Eszközök helyességének belátása 17
Mit szeretnénk elérni? Informális tervek
Informális követelmények
Formális modell
Formalizált követelmények
i
OK
Automatikus modellellenőrző
n
Ellenpélda 18
Mit szeretnénk elérni? • Alacsony szintű, vagy • magasabb szintű, vagy • mérnöki modellek
Formális modell i
OK
Automatikusan ellenőrizhető, precíz követelmények
Formalizált követelmények Automatikus modell ellenőrző
n
Ellenpélda 19
Alapmodellek Alapvető modellezési formalizmusok
21
Első lépés: modellezési formalizmus • A formalizálás célja: matematikai precizitással megadni – Modelleket: terveket, tervezői döntéseket (modellezési nyelv) – Követelményeket: elvárt tulajdonságokat (követelmény leíró nyelv)
• Formális nyelvek felépítése – Formális szintaxis – Formális szemantika
Jelölésmód: nyelvi elemek és kapcsolatok A jelölésmód interpretációja
• Mit szeretnénk leírni formális nyelvekkel? – Funkcionalitás (viselkedés, feltételek, elvárások, …) – Struktúra, interfészek – Extra-funkcionális aspektusok is: teljesítmény, megbízhatóság, …
• A formális nyelv használatának előnyei – Egyértelműség, ellenőrizhetőség – Automatikus feldolgozhatóság 22
Egy egyszerű példa • Automata formalizmus: – Állapotok és állapotátmenetek – Változók, konstansok – Feltételek az átmenetek végrehajtásához – Akciók az átmenetek végrehajtása során
23
Modellek a formális ellenőrzéshez Leképzések
Mérnöki modellek Magasabb szintű formalizmusok PN, CPN, DFN, SC Alapszintű matematikai formalizmusok KS, LTS, KTS 24
Alapszintű formalizmusok (áttekintés) • Kripke-struktúrák (KS) – Állapotok, állapotátmenetek – Állapotok lokális tulajdonságai mint címkék
• Címkézett tranzíciós rendszerek (LTS) – Állapotok, állapotátmenetek – Állapotok lokális tulajdonságai mint címkék
• Kripke tranzíciós rendszerek (KTS) – Állapotok, állapotátmenetek – Állapotok és lokális tulajdonságai mint címkék
• Véges állapotú automaták időkezeléssel – Kiterjesztések: Változók, óraváltozók, szinkronizáció 25
1. Kripke-struktúra KS, Kripke-structure: – Állapotok tulajdonságait fejezzük ki: címkézés atomi kijelentésekkel – Egy állapothoz sok címke rendelhető
Alkalmazás: Viselkedés, algoritmus leírása
KS ( S , R, L) és AP, ahol AP= P,Q,R,... atomi kijelentések halmaza (domén-specifikus) S= s1 ,s 2 ,s 3 ,...s n állapotok halmaza R S S: állapotátmeneti reláció L: S 2 AP állapotok címkézése atomi kijelentésekkel 26
Kripke-struktúra példa Közlekedési lámpa viselkedése • AP={Zöld, Sárga, Piros, Villogó} • S = {s1, s2, s3, s4, s5}
{Zöld}
{Sárga}
{Piros}
s1
s2
s3
{Piros, Sárga} s4
s5 {Villogó} 27
2. Címkézett tranzíciós rendszer LTS, Labeled Transition System: – Állapotátmenetek tulajdonságait fejezzük ki: címkézés akciókkal – Egy átmeneten csak egy akció szerepelhet
Alkalmazás: Kommunikáció, protokollok modellezése
LTS ( S , Act , ), ahol S= s1 ,s 2 ,...s n állapotok halmaza Act= a,b,c,... akciók (címkék) halmaza S Act S címkézett állapotátmenetek a
Állapotátmenetek szokásos jelölése: s1 s 2 28
LTS példák • Italautomata modelljei Act = {pénz, kávé, tea}
T1
T2 pénz
kávé
tea
pénz
kávé
pénz
tea
29
3. Kripke tranzíciós rendszer KTS, Kripke Transition System: • Állapotok és átmenetek tulajdonságait is kifejezzük: címkézés atomi kijelentésekkel és akciókkal • Egy állapothoz sok címke rendelhető, egy átmenethez egy címke rendelhető
KTS ( S , , L) és AP, Act , ahol AP P, Q, R,... atomi kijelentések halmaza (domén-specifikus) Act a, b, c,... akciók halmaza S s1 , s2 , s3 ,...sn állapotok halmaza S Act S állapotátmeneti reláció L : S 2 AP állapotok címkézése atomi kijelentésekkel 30
KTS példa • Italautomata modellje állapot címkékkel Act = {pénz, kávé, tea} AP = {Start, Választ, Stop} {Start} pénz {Választ} kávé
{Stop}
tea
{Stop} 31
Követelmények formalizálása
32
Emlékeztető: mit szeretnénk elérni? Informális tervek
Informális követelmények
Formális modell
Formalizált követelmények
i
OK
Automatikus modellellenőrző
n
Ellenpélda 33
Milyen jellegű követelményeket formalizálunk? • Verifikáció: Modell Sokféle követelmény – Funkcionális: Logikailag helyes a működés Most ez a célunk – Extra-funkcionális: Teljesítmény, megbízhatóság, … Később
• Célkitűzés: Állapotok elérhetőségének ellenőrzése – Állapotok bekövetkezési sorrendjét vizsgáljuk • Eljuthatunk-e kedvező állapotba? Élő jellegű követelmények • Elkerüljük-e a kedvezőtlen állapotokat? Biztonsági követelmények Ezek az állapottér teljes felderítésével ellenőrizhetők!
– Állapotok lokális tulajdonságára hivatkozunk • Állapot neve, állapotváltozók értéke
• Fontos állapot alapú, eseményvezérelt rendszerekben
34
„Élő” jellegű követelmények • Kívánatos helyzetek elérését írják elő – „Az indítás után a présgép kiadja az elkészült terméket.” – „A zavarás után a folyamat visszakerül stabil állapotba.”
• Egzisztenciális tulajdonság az elérhető állapotokon – „Létezik (elérhető) olyan állapot, hogy …”
• Ha egy állapotsorozat nem teljesíti: – elvileg kiegészíthető úgy, hogy teljesítse
• Közlekedési példák: – Előbb-utóbb a közlekedési lámpa zöldre vált – Szükség esetén a biztosító berendezés működésbe lép – A fékezés során a kerék megcsúszását az ECU érzékeli és aktiválja az ABS-t
36
„Biztonsági” jellegű követelmények • Veszélyes helyzetek elkerülését írják elő: – „Minden állapotban kisebb a nyomás a kritikusnál.” – „A présgép csak lecsukott ajtó mellett üzemelhet.”
• Univerzális tulajdonság az elérhető állapotokon: – „Minden elérhető állapotban igaz, hogy …” – Invariánst fogalmaznak meg
• Ha egy állapotsorozat nem teljesíti: – nem is egészíthető ki úgy, hogy teljesítse
• Közlekedési példák: – Holtpontmentesség: nem lehet minden irányból végtelen sokáig piros jelzés – Kölcsönös kizárás: keresztező irányok nem kaphatnak egyszerre zöldet 37
Az elérhetőségi követelmények leíró nyelve • Állapotok bekövetkezési sorrendjére vonatkozik – Bekövetkezési sorrend: Megfeleltethető a logikai időnek • Jelen időpillanat: Aktuális állapot • Következő időpillanat(ok): Rákövetkező állapot(ok)
– Temporális (logikai időbeli, sorrendi) operátorok használhatók a követelmények kifejezésére
• Temporális logikák: – Formális rendszer arra, hogy kijelentések igazságának logikai időbeli változását vizsgálhassuk – Temporális operátorok: „mindig”, „valamikor”, „mielőtt”, „addig, amíg”, „azelőtt, hogy”, … 38
Temporális logikák Hol értelmezhetjük a temporális logikákat? – Célkitűzés: Állapottér vizsgálata
Matematikai modell: Kripke-struktúra – Állapotok lokális tulajdonságait címkézéssel vezettük be
KS ( S , R , L ) és AP , ahol AP= P,Q,R,... atomi kijelentések halmaza (domén-specifikus) S= s1 , s 2 , s 3 ,...s n állapotok halmaza R S S : állapotátmeneti reláci ó L: S 2 AP állapotok címkézése at omi kijelentésekkel 39
Temporális logikák osztályozása • Lineáris: – A modell egy-egy végrehajtását (lefutását) tekintjük – Minden állapotnak egy rákövetkezője van – Logikai idő egy idővonal mentén (állapotsorozat) {Zöld}
{Sárga}
{Piros}
s1
s2
s3
• Elágazó:
{Piros, Sárga} s4
{Zöld}
– A modell minden lehetséges {Villogó} végrehajtását tekintjük s5 – Az állapotoknak több {Piros} rákövetkezője lehet s3 – Logikai idő elágazó idővonalak mentén jelenik meg (számítási fa)
s1
{Sárga} s2
{Villogó} s5
{Piros} s3
41
Lineáris idejű temporális logika: PLTL
42
Lineáris idejű temporális logikák • A Kripke-struktúra egy-egy útvonalán értelmezhetők – Egy-egy „lefutás” (pl. egy konkrét bemenet hatására) A modell (KS):
{Zöld}
{Sárga}
{Piros}
s1
s2
s3
{Piros, Sárga} s4
s5
{Villogó}
Egy útvonal (állapotsorozat): {Zöld}
{Sárga}
{Piros}
s1
s2
s3
{Piros, Sárga} s4
43
PLTL: Egy lineáris idejű temporális logika PLTL (Propositional Linear Time Temporal Logic) p, q, r, ... kifejezések konstruálása: • Atomi kijelentések (AP elemei): P, Q, ... • Boole logikai operátorok: , , , : És, : Vagy, : Negálás , : Implikáció
• Temporális operátorok: F, G, X, U informálisan: – – – –
F p: „Future p”, egy elérhető állapotban igaz lesz p G p: „Globally p”, minden elérhető állapotban igaz lesz p X p: „neXt p”, a következő állapotban igaz lesz p p U q: „p Until q”, egy elérhető állapotban igaz lesz q, és addig minden állapotban igaz p 44
PLTL temporális operátorok Kripke-struktúra egy útvonalán (idővonalán): P
P P
XP
P
FP GP
PUQ
P
P
P
P
P
P
P
P
P
Q
45
PLTL példák I. • p Fq Ha a kiindulási állapotra p igaz, akkor valamikor (egy későbbi állapotra) q is igaz lesz.
• G(p Fq) Minden állapotra fennáll, hogy ha p igaz, akkor valamikor q is igaz lesz. Pl. bármikor kiadott p kérésre q válasz érkezik.
• p U (q r) Itt p igaz, amíg q vagy r igaz nem lesz. Pl. az első állapotból kiadott folyamatos p kérést q válasz vagy r elutasítás követ.
• (p G(p Xp)) Gp A matematikai indukció leírása: Mindig teljesül 46
PLTL példák II. • GF p Minden állapotra igaz, hogy ebből indulva valamikor p igaz lesz. • Nem találunk olyan állapotot, ami után p tulajdonságú állapot ne lenne elérhető. • Pl. minden állapotból a p tulajdonságú kezdőállapotba vihető a rendszer.
• FG p Valamikor olyan állapotba kerül a rendszer, hogy azontúl p folyamatosan igaz lesz. • Pl. kezdeti tranziens után a p tulajdonságú üzemi állapotokba kerül a rendszer.
47
Követelmények formalizálása: Példa Adott egy klímaberendezés, aminek a következő üzemmódokat kell biztosítania: AP={Kikapcsolva, Bekapcsolva, Elromlott, GyengénHűt, ErősenHűt, Fűt, Szellőztet} • Egy-egy állapothoz több címke tartozhat! • A követelmény formalizálás fázisában a teljes (valós) viselkedést még nem ismerjük épp az a cél, hogy a követelményeknek megfelelően tervezzük meg! 48
Példa (folytatás) AP={Kikapcsolva, Bekapcsolva, Elromlott, GyengénHűt, ErősenHűt, Fűt, Szellőztet}
• A klímát be fogják kapcsolni: F (Bekapcsolva) • A klíma előbb-utóbb mindig elromlik: G F (Elromlott) • Ha a klíma elromlik, mindig megjavítják:
G (Elromlott F (Elromlott)) • Ha a klíma elromlott, nem fűthet: G ((Elromlott Fűt)) 49
Példa (folytatás) AP={Kikapcsolva, Bekapcsolva, Elromlott, GyengénHűt, ErősenHűt, Fűt, Szellőztet}
• A klíma csak úgy romolhat el, ha be volt kapcsolva: G ( X Elromlott Bekapcsolva) • A fűtési fázis befejezésekor szellőztetni kell:
G ((Fűt X(Fűt)) X (Szellőztet)) de el is romolhat: G ((Fűt X(Fűt)) X (Szellőztet Elromlott))
• Szellőztetés után mindaddig nem hűthet erősen, míg egy gyenge hűtéssel nem próbálkozott: G ((Szellőztet X(Szellőztet)) X(ErősenHűt U GyengénHűt)) 50
Elágazó idejű temporális logikák: CTL, CTL*
51
Ismétlés: Temporális logikák osztályozása • Lineáris idejű: – A modell egy-egy végrehajtását (lefutását) tekintjük – Minden állapotnak egy rákövetkezője van – Logikai idő egy idővonal mentén (állapotsorozat) {Zöld}
{Sárga}
{Piros}
s1
s2
s3
• Elágazó idejű:
{Piros, Sárga} s4
{Zöld}
– A modell minden lehetséges {Villogó} végrehajtását tekintjük s5 – Az állapotoknak több {Piros} rákövetkezője lehet s3 – Logikai idő elágazó idővonalak mentén jelenik meg (számítási fa)
s1
{Sárga} s2
{Villogó} s5
{Piros} s3
52
Számítási fa konstrukciója Kripkestruktúra:
{Zöld}
{Sárga}
{Piros}
s1
s2
s3
{Piros, Sárga} s4
s5
{Villogó} {Zöld}
Számítási fa: Lehetséges elágazások
s1
{Villogó}
{Sárga}
s5
s2
{Piros}
{Villogó} s3
{Piros,Sárga} s4
s5
{Villogó} s5
{Piros} s3
{Piros} s3
{Piros,Sárga} s4
{Villogó} s5
53
Elágazások vizsgálata Egy-egy állapotban előírható, hogy az útvonalakra vonatkozó p követelmény hány onnan kiinduló útvonal mentén teljesüljön: • E p (Exists p): Létezzen legalább egy útvonal, ahol a p követelmény teljesül – Egy lehetséges továbblépés mentén vizsgál – Egzisztenciális operátor
s
• A p (forAll p): Minden útvonalra fennálljon, hogy a p követelmény teljesül – Minden lehetséges továbblépést magába foglal – Univerzális operátor
s
54
Elágazó idejű temporális logikák • CTL*: Computational Tree Logic * – Útvonal kvantorok (E, A), és – útvonalakon értelmezett temporális operátorok (F, G, X, U) tetszőleges kombinációja
• CTL: Computational Tree Logic – Útvonalakon értelmezett temporális operátorokat mindig közvetlenül meg kell előznie útvonal kvantoroknak – Útvonalakon értelmezett operátorok nem kombinálhatók 55
CTL*: Computational Tree Logic *
56
CTL* operátorok (informális) • Útvonalak kvantorai (állapotokon értelmezett): – A: „for All futures”, minden lehetséges útra az adott állapotból kiindulva – E: „Exists future”, „for some future”, legalább egy útra az adott állapotból kiindulva
• Útvonalakon értelmezett operátorok: – – – –
F p: „Future”, valamikor az útvonal egy állapotán p igaz G p: „Globally”, az útvonal minden állapotán p igaz X p: „neXt”, a következő állapotban p igaz p U q: „p Until q”, az útvonal egy állapotán igaz lesz q, és addig minden állapotban igaz p 57
CTL* kifejezések
A(p F q) Minden útvonalra igaz, hogy …
amennyiben p fennáll az útvonal elején, …
akkor ezt a jövőben olyan állapot fogja követni …
amelyben, vagy ahonnan indulva található olyan állapot, amelyben q fennáll.
58
Példa CTL* kifejezések • E(p G q) Létezik olyan útvonal, hogy ezen p fennáll (az útvonal elejétől nézve) és az útvonal minden szuffixén q is fennáll
• E(XXX p F q) Létezik olyan útvonal, hogy – vagy ennek negyedik állapotán fennáll p,
– vagy valamikor q fennáll az útvonalon
59
CTL: Computational Tree Logic
63
Háttér: Az ellenőrzés komplexitása • CTL* ellenőrzése túl nehéz! • Worst-case időkomplexitás: Legalább O (|S|2 2|p|) – |S|2 az átmenetek száma a modellben (Kripke-struktúrában) worst case esetben – |p| az operátorok száma a temporális logikai kifejezésben
• Az exponenciális komplexitás riasztó – Bár a temporális logikai kifejezések tipikusan rövidek
• Célkitűzés: A CTL* egyszerűsítése – Gyakorlati problémák esetén használható maradjon – Az ellenőrzés worst-case időkomplexitása csökkenjen 64
CTL operátorok (informális bevezető) Állapotokon értelmezhető összetett operátorok: • EX p: létezik útvonal, aminek következő állapotán p • EF p: létezik útvonal, aminek jövőbeli állapotán p • EG p: létezik útvonal, aminek minden állapotán p • E(p U q): létezik útvonal, amin p amíg q • • • •
AX p: minden útvonal következő állapotán p AF p: minden útvonal egy-egy jövőbeli állapotán p AG p: minden útvonal minden állapotán p A(p U q): minden útvonalon p amíg q 65
CTL operátorok (példák)
EX P
EF P
EG P
AX P
AF P
AG P
66
CTL kifejezések (példák) • AG EF p Bárhonnan indulva olyan állapotba vihető a rendszer, ahol p igaz • Pl. AG EF Reset
• AG AF p Bárhonnan indulva mindenképpen eljutunk olyan állapotba, ahol p igaz • Pl. AG AF Terminated
• AG (p AF q) Bárhonnan indulva teljesül, hogy ha ott p igaz, akkor valamikor mindenképpen elérünk olyan állapotba, ahol q igaz. • Pl. AG (Request AF Reply) 68
CTL kifejezések (példák) • EF AG p Lehetséges, hogy a rendszer olyan állapotba kerül, hogy utána p minden állapotban igaz lesz
• AF AG p Bármely úton haladva eljutunk olyan állapotba, hogy utána p mindig igaz lesz • Pl. AF AG Normal
• AG (p A (p U q)) Bármelyik elérhető állapotban ha p igaz, akkor minden úton p fennáll q eléréséig • „p fennáll q eléréséig” pontosabban: elérünk egy olyan állapotba, ahol q igaz, és addig minden állapotban p igaz 69
Követelmények formalizálása: Egy példa • Két processzből álló rendszer: P1 és P2 • Processz állapotok a követelmények szempontjából: – Kritikus szakaszban van: C1, C2 – Nem-kritikus szakaszban van: N1, N2 – Kritikus szakaszba belépésre kész: W1, W2
• Atomi kijelentések: AP = {C1, C2, N1, N2, W1, W2}
70
Mintapélda (folytatás) • Egyszerre csak egy processz lehet a kritikus szakaszban: AG ((C1 C2)) • Ha egy processz be akar lépni a kritikus szakaszba, akkor előbb-utóbb mindig beléphet: AG (W1 AF(C1)) AG (W2 AF(C2)) • A processzek mindig felváltva kerülnek a kritikus szakaszba; egyikük kilép majd a másik lép be: AG(C1 A(C1 U (C1 A((C1) U C2)))) AG(C2 A(C2 U (C2 A((C2) U C1)))) 71
Mintapélda (folytatás) • Egyszerre csak egy processz lehet a kritikus szakaszban: AG ((C1 C2))P1 nincs a kritikus • Ha egy processzszakaszban be akar lépni a kritikus szakaszba, P2 lép a kritikus akkor előbb-utóbb mindig beléphet: szakaszba P1 a kritikus AGvan (W1 AF(C1)) szakaszban AG (W2 AF(C2)) • A processzek mindig felváltva kerülnek a kritikus szakaszba; egyikük kilép majd a másik lép be: AG(C1 A(C1 U (C1 A((C1) U C2)))) AG(C2 A(C2 U (C2 A((C2) U C1)))) 72
Formális módszerek értékelése Mit várhatunk? Korlátok, sikertörténetek
73
Amik a formális vizsgálatot nehézzé teszik… • Valósághű modellezés – Ismeretek hiánya, feltételezések (pl. a környezetről) – De: Formális módszerek használatától független ez a probléma
• Speciális ismereteket igényel a felhasználótól – Alacsony szintű matematikai modellek, jelölésrendszer – De: Mérnöki modellezési nyelvek eltakarhatják
• Bonyolultak az ellenőrzés és szintézis módszerei – Algoritmusok, technikák korlátait ismerni kell – Kézi beavatkozásra lehet szükség (pl. tételbizonyító rendszerek) – De: Terjednek a „gombnyomásra működő” eszközök
• Csak „kisméretű” problémákra alkalmazható – Modell, állapottér kezelhető-e a meglévő erőforrásokkal – De: Eszközök hatékonysága folyamatosan nő 74
Jelen helyzet • Megkötések – Diszkrét állapotú – Diszkrét idejű – Diszkrét eseményterű
rendszerek (DES)
• Kihívások, kutatási területek – – – – –
Matematikai algoritmusok hatékonysága és szintje Modell osztályok korlátai (pl. időzítés) Modell készítés nehézsége (pl. absztrakció) Nyelvek kifejezőképessége (pl. VHDL) Nyelvek nem pontos definíciója (pl. UML)
75
Modellek a formális ellenőrzéshez • Rendszermodellek – Mérnöki modellek: • Pl. UML diagramok (fél-)formális szemantikával
– Magasabb szintű modellek: • Vezérlés orientált: Automata, Petri-háló, … • Adatfeldolgozás orientált: Adatfolyam háló, … • Kommunikáció orientált: Processz algebra, …
– Alapszintű matematikai modellek: • KS, LTS, KTS, automaták, Büchi automaták
• Tulajdonság leírások – Magasabb szintű: • Idődiagram, üzenet szekvencia diagram (MSC)
– Alapszintű: • Elsőrendű logika, temporális logika, referencia automata 76
A formális verifikáció fejlődése • A SAT eszközök (kielégíthetőség) lehetőségei: Változók száma
100000 10000 1000 100 10 1 1960
1970
1980
Év
1990
2000
2010
• Modellellenőrző eszközök képességei: – 1020 266 méretű állapottér (ROBDD-vel, 1990) – 10100 2328 méretű állapottér speciális esetben – 1062900 méretű állapottérre is volt példa (MIT TDK) 77
Sikertörténetek
78
Sikeres megközelítés Rendszer tervezése Mérnöki modell (pl. UML)
Formális ellenőrzés Automatikus modellgenerálás
Eredmények visszavezetése
Formális modell
Analízis
Megvalósítás int main() { while (i
Implementáció 79
Klasszikus alkalmazások • USA TCAS-II forgalomirányító rendszer
– RSML nyelven specifikált; teljesség és ellentmondás-mentesség ellenőrzése
• Philips Audio Protocol
– 1994: manuális verifikáció, majd 1996: automatikus ellenőrzés (HyTech)
• Lockheed C130J repülési szoftvere
– Programfejlesztés helyességbizonyítással (CORE spec. nyelv + Ada) – Költség nem nőtt a tesztelés egyszerűsödése miatt
• IEEE Futurebus+ szabvány
– Carnegie Mellon SMV: cache koherencia protokoll hibájának kiderítése
• Hardver projektek: ACL2 automatikus tételbizonyító
– Motorola DSP Complex Arithmetic Processor mag (250 regiszter): DSP algoritmusok ellenőrzése – AMD 5K86 processzor: Lebegőpontos osztás algoritmusának ellenőrzése
• Intel Core i7 processzor
– „For the recent Intel CoreTM i7 design we used formal verification as the primary validation vehicle for the core execution cluster” – Szimbolikus szimuláció az adatutak teljes vizsgálatára (2700 mikroutasítás, 20 mérnökévnyi munka) – Binary Decision Diagram alkalmazása
• Modell alapú szoftverfejlesztéshez kapcsolódó eszközök – IBM, Esterel, Prover, Mentor, Verum, Telelogic, …
80
Forráskódhoz illeszkedő formális verifikáció • Java
– Bandera, PathFinder: modell absztrakció – Java VM formalizálása: Abstract State Machine
• Ada
– SPARK Ada verification condition generator tételbizonyítóhoz
• C
– BLAST: Szoftver modellellenőrző C programokhoz (absztrakció) – CBMC: C alapú korlátos modellellenőrző
• C#, Visual Basic .Net
– Zing (MS Visual Studio-hoz): Konkurens szoftver modellellenőrzése
• Spec# (C# superset)
– MS Research Boogie 2: Specifikációs nyelvi kiterjesztések – Helyességi kritériumok ellenőrzése: program absztrakcióval és tételbizonyítóval (Z3)
• Microsoft Windows Driver Kit (WDK)
– Static Driver Verifier Research Platform, SLAM 2 eszköz – Windows API használati feltételeinek statikus ellenőrzése
81
Összefoglalás • Mik a formális módszerek? – Formalizmus, formális nyelv – Formális módszerek és eszközök: Szimuláció, formális verifikáció, szintézis
• Mire használhatók? – Motiváció: Szoftver minőségi kihívások – A formális módszerek lehetőségei
• Mit várhatunk? – Korlátok – Sikertörténetek
82
