Informatika pro z´achranu ˇzivota Stefan Ratschan ´ Ustav Informatiky Akademie Vˇ ed
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
1 / 15
Katastrofick´y zaˇc´atek.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
2 / 15
Therac-25
I
Zaˇr´ızen´ı pro radioterapii
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
3 / 15
Therac-25
I I
Zaˇr´ızen´ı pro radioterapii P˚ uvodn´ı zaˇr´ızen´ı (therac-20) skoro v´yhradnˇe mechanick´e.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
3 / 15
Therac-25
I I I
Zaˇr´ızen´ı pro radioterapii P˚ uvodn´ı zaˇr´ızen´ı (therac-20) skoro v´yhradnˇe mechanick´e. Pozorov´an´ı: Mechanick´y pˇr´ıstroj nebezpeˇcn´y (opotˇrebuje se), softwarov´e ˇr´ızen´ı.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
3 / 15
Therac-25
I I I
I
Zaˇr´ızen´ı pro radioterapii P˚ uvodn´ı zaˇr´ızen´ı (therac-20) skoro v´yhradnˇe mechanick´e. Pozorov´an´ı: Mechanick´y pˇr´ıstroj nebezpeˇcn´y (opotˇrebuje se), softwarov´e ˇr´ızen´ı. V´ysledek?
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
3 / 15
Therac-25
I I I
I
Zaˇr´ızen´ı pro radioterapii P˚ uvodn´ı zaˇr´ızen´ı (therac-20) skoro v´yhradnˇe mechanick´e. Pozorov´an´ı: Mechanick´y pˇr´ıstroj nebezpeˇcn´y (opotˇrebuje se), softwarov´e ˇr´ızen´ı. V´ysledek? Alespoˇ n 6 hav´ari´ı s nadmˇernou d´avkou radiace, nˇekter´e z nich smrteln´e.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
3 / 15
Ariane 5 let 501 (1996)
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
4 / 15
Ariane 5 let 501 (1996)
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
4 / 15
Ariane 5 let 501 (1996)
I
Let skonˇcil nˇekolik des´ıtek sekund po startu exploz´ı ˇ Skoda: 290 Me
I
Odklad programu jeden rok
I
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
4 / 15
Northeast Blackout of 2003
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
5 / 15
Northeast Blackout of 2003
I
I I
V´ypadek proudu ve velk´e ˇc´asti Spojen´ych st´at˚ u americk´ych 14.-16.8.2003 V´ıc neˇz 10 pˇrim´ych u ´mrt´ı Obrovsk´e finanˇcn´ı ˇskody
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
5 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou?
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla. Raketa mˇela dva redundantn´ı poˇc´ıtaˇce
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla. Raketa mˇela dva redundantn´ı poˇc´ıtaˇce (stejn´y probl´em v obou).
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla. Raketa mˇela dva redundantn´ı poˇc´ıtaˇce (stejn´y probl´em v obou). Ariane 5 (na rozd´ıl od verze 4) tuto softwarovou funkcionalitu uˇz ani nepotˇrebovala.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Souvislost Co to m´a spoleˇcn´eho s informatikou? I
Kaˇzd´a nadmˇern´a d´avka v Therac-25 byla v´ysledkem chyby v ˇr´ıd´ıc´ım softwaru. Nebezpeˇcn´y stav byl dˇr´ıve vylouˇcen mechanick´ym zaˇr´ızen´ım.
I
Exploze Ariane 5 byla v´ysledkem chybn´e konverze z ˇc´ısla s pohyblivou ˇc´arkou do cel´eho ˇc´ısla. Raketa mˇela dva redundantn´ı poˇc´ıtaˇce (stejn´y probl´em v obou). Ariane 5 (na rozd´ıl od verze 4) tuto softwarovou funkcionalitu uˇz ani nepotˇrebovala.
I
V´ypadek proudu v´ysledkem pozdn´ı reakce na menˇs´ı probl´em kv˚ uli chybˇe v softwaru poplachov´eho zaˇr´ızen´ı.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
6 / 15
Cyber-Physical Systems (CPS) ˇ ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ C´ u
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
7 / 15
Cyber-Physical Systems (CPS) ˇ ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ C´ u
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
7 / 15
Cyber-Physical Systems (CPS) ˇ ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ C´ u
N´aklady na elektroniku/software vyˇsˇs´ı neˇz fyzick´e auto.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
7 / 15
Cyber-Physical Systems (CPS) ˇ ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ C´ u
N´aklady na elektroniku/software vyˇsˇs´ı neˇz fyzick´e auto. Dnes: Vˇetˇsina v´ypoˇcetn´ı kapacity se uˇz nenach´az´ı ve stoln´ıch poˇc´ıtaˇc´ıch
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
7 / 15
Safety Critical System
Nejen, ˇc´ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ u, ale i integrace do kaˇzdodenn´ıho lidsk´eho ˇzivota
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
8 / 15
Safety Critical System
Nejen, ˇc´ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ u, ale i integrace do kaˇzdodenn´ıho lidsk´eho ˇzivota Poruchy mohou ohroˇzovat lidsk´y ˇzivot
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
8 / 15
Safety Critical System
Nejen, ˇc´ım d´al vˇetˇs´ı integrace digitaln´ı elektroniky/softwaru a fyzik´aln´ıch syst´em˚ u, ale i integrace do kaˇzdodenn´ıho lidsk´eho ˇzivota Poruchy mohou ohroˇzovat lidsk´y ˇzivot Spr´avnost nezbytn´a
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
8 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy:
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
I
velmi ˇspinav´e pr´adlo, skoro ˇcist´e pr´adlo
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
I
velmi ˇspinav´e pr´adlo, skoro ˇcist´e pr´adlo
I
kdyˇz stoj´ı u ´plnˇe vodorovnˇe, kdyˇz ne
9 / 15
Zakl´ad´ame podnik na praˇcky
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
I
velmi ˇspinav´e pr´adlo, skoro ˇcist´e pr´adlo
I
kdyˇz stoj´ı u ´plnˇe vodorovnˇe, kdyˇz ne
I
...
9 / 15
Zakl´ad´ame podnik na praˇcky Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
I
velmi ˇspinav´e pr´adlo, skoro ˇcist´e pr´adlo
I
kdyˇz stoj´ı u ´plnˇe vodorovnˇe, kdyˇz ne
... Pˇredpoklad: 15 takov´ych parametr˚ u, jen 2 hodnoty, kaˇzd´y pokus trv´a hodinu, stoj´ı 20e.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
I
9 / 15
Zakl´ad´ame podnik na praˇcky Dˇr´ıve neˇz je prod´av´ame, mus´ıme zjistit, jestli funguj´ı Pˇred-poˇc´ıtaˇcov´y vˇek: pokusy s prototypy: I
teploty: 40◦ , 60◦ , 90◦
I
s tvrdou vodou, s mˇekkou vodou
I
hodnˇe pr´adla, m´alo pr´adla
I
velmi ˇspinav´e pr´adlo, skoro ˇcist´e pr´adlo
I
kdyˇz stoj´ı u ´plnˇe vodorovnˇe, kdyˇz ne
... Pˇredpoklad: 15 takov´ych parametr˚ u, jen 2 hodnoty, kaˇzd´y pokus trv´a hodinu, stoj´ı 20e. I
Pak: 1365 dny (>3 roky) testov´an´ı, skoro 1 Me
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
9 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry:
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
I
Praˇcka je relativnˇe jednoduch´y stroj vlaky, letadla, . . . : nˇekolik tis´ıc parametr˚ u, selh´an´ı m´a za n´asledek katastrofu!
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
I
Praˇcka je relativnˇe jednoduch´y stroj vlaky, letadla, . . . : nˇekolik tis´ıc parametr˚ u, selh´an´ı m´a za n´asledek katastrofu!
V okamˇziku, kdy uˇz nem˚ uˇzeme d´al, pˇrijde
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
I
Praˇcka je relativnˇe jednoduch´y stroj vlaky, letadla, . . . : nˇekolik tis´ıc parametr˚ u, selh´an´ı m´a za n´asledek katastrofu!
V okamˇziku, kdy uˇz nem˚ uˇzeme d´al, pˇrijde: poˇc´ıtaˇc!
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
I
Praˇcka je relativnˇe jednoduch´y stroj vlaky, letadla, . . . : nˇekolik tis´ıc parametr˚ u, selh´an´ı m´a za n´asledek katastrofu!
V okamˇziku, kdy uˇz nem˚ uˇzeme d´al, pˇrijde: poˇc´ıtaˇc! Pokusy na poˇc´ıtaˇci: simulace, testov´an´ı
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Testov´an´ı Tvrdost vody, objem pr´adla, ˇspinavost pr´adla, n´aklon praˇcky atd.: Parametry: I
Nejsou jen 2, 4, 234, 10231, . . . moˇzn´e hodnoty. I kdyˇz vyb´ır´ame jak´ykoli poˇcet hodnot pro testy, m˚ uˇzeme vˇzdy minout probl´emovou hodnotu.
I
V´yvoj v ˇcase!
I
Praˇcka je relativnˇe jednoduch´y stroj vlaky, letadla, . . . : nˇekolik tis´ıc parametr˚ u, selh´an´ı m´a za n´asledek katastrofu!
V okamˇziku, kdy uˇz nem˚ uˇzeme d´al, pˇrijde: poˇc´ıtaˇc! Pokusy na poˇc´ıtaˇci: simulace, testov´an´ı Potˇrebujeme model (poˇc´ıtaˇcov´a reprezentace praˇcky) ´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
10 / 15
Model: Mikroˇcip pro ˇr´ızen´ı ot´aˇcek zvyseni vykonu
otacky≥ 2.2
otacky ≤ 1.5 nalozeni zachovani vykonu
otacky ≤ 1.8
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
otacky ≥ 2.5
snizeni vykonu
11 / 15
Model: Mikroˇcip pro ˇr´ızen´ı ot´aˇcek zvyseni vykonu
otacky≥ 2.2
otacky ≤ 1.5 nalozeni zachovani vykonu
otacky ≤ 1.8
otacky ≥ 2.5
snizeni vykonu
Diskr´etn´ı: dobˇre oddˇelen´e stavy, nav´ıc: koneˇcn´y poˇcet
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
11 / 15
Modelov´an´ı v´yvoje ot´aˇcek Zat´ım popisujeme (tj. modelujeme) jen zmˇenu v´ykonu.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
12 / 15
Modelov´an´ı v´yvoje ot´aˇcek Zat´ım popisujeme (tj. modelujeme) jen zmˇenu v´ykonu. V´yvoj poˇctu ot´aˇcek?
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
12 / 15
Modelov´an´ı v´yvoje ot´aˇcek Zat´ım popisujeme (tj. modelujeme) jen zmˇenu v´ykonu. V´yvoj poˇctu ot´aˇcek? otacky s
t
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
12 / 15
Modelov´an´ı v´yvoje ot´aˇcek Zat´ım popisujeme (tj. modelujeme) jen zmˇenu v´ykonu. V´yvoj poˇctu ot´aˇcek? otacky s
t
Spojit´y model
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
12 / 15
Modelov´an´ı v´yvoje ot´aˇcek Zat´ım popisujeme (tj. modelujeme) jen zmˇenu v´ykonu. V´yvoj poˇctu ot´aˇcek? otacky s
t
Spojit´y model ˇ Casto se pouˇz´ıvaj´ı diferenci´aln´ı rovnice x˙ = f (x) ´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
12 / 15
Model: Hybridn´ı syst´em zvyseni vykonu
˙ otacky = f + (otacky ) otacky≥ 2.2
otacky = 0
otacky ≤ 1.5
nalozeni zachovani vykonu
˙ otacky = 0
˙ otacky = f0 (otacky )
otacky ≤ 1.8
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
otacky ≥ 2.5
snizeni vykonu
˙ otacky = f − (otacky )
13 / 15
Simulace: Pokusy na modelu
Demo: Scicos
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Simulace: Pokusy na modelu
Demo: Scicos V´yhoda: levnˇejˇs´ı, rychlejˇs´ı, bezpeˇcnˇejˇs´ı neˇz pokusy
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Simulace: Pokusy na modelu
Demo: Scicos V´yhoda: levnˇejˇs´ı, rychlejˇs´ı, bezpeˇcnˇejˇs´ı neˇz pokusy Probl´em: Simulace sice pom´ahaj´ı naj´ıt chyby
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Simulace: Pokusy na modelu
Demo: Scicos V´yhoda: levnˇejˇs´ı, rychlejˇs´ı, bezpeˇcnˇejˇs´ı neˇz pokusy Probl´em: Simulace sice pom´ahaj´ı naj´ıt chyby Ale: nikdy si nem˚ uˇzeme b´yt jisti, jestli jsme uˇz naˇsli vˇsechny chyby
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Simulace: Pokusy na modelu
Demo: Scicos V´yhoda: levnˇejˇs´ı, rychlejˇs´ı, bezpeˇcnˇejˇs´ı neˇz pokusy Probl´em: Simulace sice pom´ahaj´ı naj´ıt chyby Ale: nikdy si nem˚ uˇzeme b´yt jisti, jestli jsme uˇz naˇsli vˇsechny chyby Souˇcasn´ı v´yzkum: Form´aln´ı verifikace hybridn´ıch syst´em˚ u: matematick´y d˚ ukaz spr´avnosti, automaticky na poˇc´ıtaˇci
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Simulace: Pokusy na modelu
Demo: Scicos V´yhoda: levnˇejˇs´ı, rychlejˇs´ı, bezpeˇcnˇejˇs´ı neˇz pokusy Probl´em: Simulace sice pom´ahaj´ı naj´ıt chyby Ale: nikdy si nem˚ uˇzeme b´yt jisti, jestli jsme uˇz naˇsli vˇsechny chyby Souˇcasn´ı v´yzkum: Form´aln´ı verifikace hybridn´ıch syst´em˚ u: matematick´y d˚ ukaz spr´avnosti, automaticky na poˇc´ıtaˇci Model nem´a ˇz´adn´y v´yvoj do nebezpeˇcn´ıho stavu.
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
14 / 15
Z´avˇer
Zajiˇstˇen´ı spr´avnosti technick´ych syst´em˚ u: I
Pokusy (drah´e, nebezpeˇcn´e, omezen´a jistota)
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
15 / 15
Z´avˇer
Zajiˇstˇen´ı spr´avnosti technick´ych syst´em˚ u: I
Pokusy (drah´e, nebezpeˇcn´e, omezen´a jistota)
I
Simulace (potˇrebujeme model, levnˇejˇs´ı, omezen´a jistota)
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
15 / 15
Z´avˇer
Zajiˇstˇen´ı spr´avnosti technick´ych syst´em˚ u: I
Pokusy (drah´e, nebezpeˇcn´e, omezen´a jistota)
I
Simulace (potˇrebujeme model, levnˇejˇs´ı, omezen´a jistota)
I
Form´aln´ı verifikace (matematick´y d˚ ukaz spr´avnosti)
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
15 / 15
Z´avˇer
Zajiˇstˇen´ı spr´avnosti technick´ych syst´em˚ u: I
Pokusy (drah´e, nebezpeˇcn´e, omezen´a jistota)
I
Simulace (potˇrebujeme model, levnˇejˇs´ı, omezen´a jistota)
I
Form´aln´ı verifikace (matematick´y d˚ ukaz spr´avnosti)
Proslul´y tzv. kachˇ n´atkov´y probl´em:
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
15 / 15
Z´avˇer
Zajiˇstˇen´ı spr´avnosti technick´ych syst´em˚ u: I
Pokusy (drah´e, nebezpeˇcn´e, omezen´a jistota)
I
Simulace (potˇrebujeme model, levnˇejˇs´ı, omezen´a jistota)
I
Form´aln´ı verifikace (matematick´y d˚ ukaz spr´avnosti)
Proslul´y tzv. kachˇ n´atkov´y probl´em: Pokud verifikace nevyjde (protoˇze syst´em chybu m´a), co se m˚ uˇzeme nauˇcit (tj. jak m˚ uˇzeme z toho tu chybu naj´ıt)?
´ Stefan Ratschan (Ustav Informatiky Akademie Vˇ ed)
15 / 15
