Véges és determinisztikus diszkrét eseményrendszer specifikáció - Finite & Deterministic Discrete Event System Specification

Az FD-DEVS (véges és determinisztikus diszkrét eseményrendszer-specifikáció) egy formalizmus a diszkrét eseménydinamikai rendszerek modellezésére és elemzésére mind szimulációs, mind ellenőrzési módszerekkel. Az FD-DEVS moduláris és hierarchikus modellezési funkciókat is kínál, amelyeket a Classic DEVS- től örököltek .

Történelem

Az FD-DEVS-t eredetileg "Schedule-Controllable DEVS" -ként [Hwang05] nevezték el, és célja az volt, hogy támogassa hálózatainak hitelesítési elemzését, amely 30 évig nyitott probléma volt a DEVS-formalizmusban. Ezenkívül kijelölték az SP-DEVS úgynevezett " OPNA " problémájának megoldására is . A klasszikus DEVS szempontjából az FD-DEVS-nek három korlátozása van

1. az eseményhalmazok és az állapothalmaz végessége,
2. egy állapot élettartama racionális számmal vagy végtelenül ütemezhető, és
3. a belső ütemtervet megőrizheti vagy frissítheti egy bemeneti esemény.

A harmadik korlátozás az SP-DEVS-től való kikapcsolódásnak is tekinthető, ahol az ütemtervet mindig megőrzik bármilyen bemeneti esemény. Ennek a relaxációnak a következtében már nincs OPNA probléma, de van egy korlátozás is, miszerint az SP-DEVS hálózatok eltelt idõinek elvonására használható idõvonal-absztrakció az FD-DEVS hálózat számára már nem hasznos [Hwang05] . De egy másik idő absztrakciós módszer [Dill89], amelyet D. Dill professzor talált ki, alkalmazható az FD-DEVS hálózatok véges csúcsú elérhetőségi grafikonjának megszerzésére.

Példák

Ping-pong játék

1. ábra: FD-DEVS csatolt ábra a ping-pong játékhoz

Vegyünk egy ping-pong mérkőzést, amelyben két játékos van. Minden játékos modellezhető FD-fejlesztőkkel, hogy a játékos modell bemeneti esemény ? Kapnak és egy kimeneti esemény ! Send , és ez a két állam: Küldés és Wait . Amint a játékos belép a "Küldés" -be, generál egy "! Küldés" -et, és visszatér a "Várakozás" -ra a küldési idő után, amely 0,1 időegység. Ha a "Várj" -nál tartózkodik, és ha "? Fogadja", akkor újra "Küldés" -re változik. Más szavakkal, a játékos modell örökre a "Várjon" marad, hacsak nem kapja meg?

A teljes ping-pong mérkőzés elérése érdekében az egyik játékos elkövetőként kezd, akik kezdeti állapota „Küldés”, a másik pedig olyan védőként indul, akiknek kezdeti állapota „Várakozás”. Így az 1. ábrán az A játékos a kezdő elkövető, a B játékos pedig a kezdő védő. Ezenkívül a játék folytatása érdekében minden játékos "? Send" eseményét össze kell kapcsolni a másik játékos "? Fogadásával" az 1. ábra szerint.

Két nyílású kenyérpirító

2. ábra: (a) Kéthelyes kenyérpirító (b) FD-DEVS összekapcsolt ábra a kéthelyes kenyérpirítóhoz

Vegyünk egy kenyérpirítót, amelyben két nyílás van, amelyeknek saját indítógombjai vannak, amint az a 2. ábra (a) ábrán látható. Minden rés azonos funkcióval rendelkezik, kivéve a pirítás idejét. Kezdetben a gombot nem nyomják meg, de ha valaki megnyomja a gombot, a hozzá tartozó rés megkezdi a pirítás idejét: 20 másodperc a bal oldalsó, 40 másodperc a jobb rés esetén. A pirítási idő után minden rés és annak gombjai felbukkannak. Figyelje meg, hogy bár az ember megpróbál nyomni egy gombot, amikor a hozzá tartozó nyílás pirít, semmi sem történik.

Modellezhetjük FD-DEVS-sel, ahogy a 2. ábra (b) ábra mutatja. Két rés atomi FD-DEVS-ként van modellezve, amelyek bemeneti eseménye "? Push", a kimeneti esemény pedig "! Pop", az állapotok pedig "Idle" (I) és "Toast" (T) a kezdeti állapot "tétlen". Amikor "üresjárat" és "? Push" -ot kap (mert az egyik megnyomja a gombot), az állapota "Toast" -ra változik. Más szavakkal, örökké az "üresjáratban" marad, hacsak nem kapja meg a "? Push" eseményt. 20 (40. kép) másodperc múlva a bal (jobb. Jobb) rés visszatér az „alapjáratra”.

Atomic FD-DEVS

Formális meghatározás

${\ displaystyle M = <X, Y, S, s_ {0}, \ tau, \ delta _ {x}, \ delta _ {y}>}$

ahol

• ${\ displaystyle X}$van egy véges halmaza bemeneti eseményeket ;
• ${\ displaystyle Y}$van egy véges halmaza kimeneti események ;
• ${\ displaystyle S}$van egy véges halmaza ;
• ${\ displaystyle s_ {0} \ in S}$van a kezdeti állapotban ;
• ${\ displaystyle \ tau: S \ rightarrow \ mathbb {Q} _ {[0, \ infty]}}$az időelőleges függvény, amely meghatározza egy olyan állapot élettartamát, ahol a nem negatív racionális számok halmaza plusz a végtelen.${\ displaystyle \ mathbb {Q} _ {[0, \ infty]}}$
• ${\ displaystyle \ delta _ {x}: S \ x X \ rightarrow S \ times \ {0,1 \}}$a külső átmeneti függvény , amely meghatározza, hogy egy bemeneti esemény megváltoztatja a menetrend, valamint a rendszer állapotát. Az állapot belső ütemezését frissítik, ha ellenkező esetben (azaz ) megmarad az ütemezés.${\ displaystyle s \ in S}$${\ displaystyle \ tau (s)}$${\ displaystyle \ delta _ {x} (s) = (s ', 1)}$${\ displaystyle \ delta _ {x} (s) = (s ', 0)}$
• ${\ displaystyle \ delta _ {y}: S \ jobbra nyíl Y ^ {\ phi} \ szor S}$a kimeneti és a belső átmeneti függvény , ahol és jelöli a csendes eseményt . A kimeneti és a belső átmeneti függvény meghatározza, hogy egy állapot hogyan generál kimeneti eseményt, ugyanakkor hogyan változik az állapot belsőleg.${\ displaystyle Y ^ {\ phi} = Y \ csésze \ {\ phi \}}$${\ displaystyle \ phi \ notin Y}$

A Ping-Pong Player hivatalos képviselete

Az 1. ábrán látható ping-pong példában a játékos formális ábrázolása a következőképpen adható meg. ahol = {? kapni}; = {! küldés}; = {Küldés, várás}; = Küldés az A játékoshoz, Várjon a B játékoshoz; (Küldés) = 0,1, (Várjon) = ; (Várjon, fogadjon) = (Küldés, 1), (Küldés,? Fogadás) = (Küldés, 0); (Küldés) = (! Küld, Várj), (Várj) = ( , Várj). ${\ displaystyle M = <X, Y, S, s_ {0}, \ tau, \ delta _ {x}, \ delta _ {y}>}$${\ displaystyle X}$${\ displaystyle Y}$${\ displaystyle S}$${\ displaystyle s_ {0}}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ infty}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ phi}$

Egy kenyérpirító hivatalos ábrázolása

A kétrekeszes kenyérpirító résének hivatalos ábrázolása a 2. ábra (a) és (b) ábráján az alábbiak szerint adható meg. ahol = {? push}; = {! pop}; = {I, T}; = I; (T) = 20 a bal résnél, 40 a jobb résnél, (I) = ; (I, P push) = (T, 1), (T, P push) = (T, 0); (T) = (! Pop, I), (I) = ( , I). ${\ displaystyle M = <X, Y, S, s_ {0}, \ tau, \ delta _ {x}, \ delta _ {y}>}$${\ displaystyle X}$${\ displaystyle Y}$${\ displaystyle S}$${\ displaystyle s_ {0}}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ infty}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ phi}$

A Crosswalk Light Controller hivatalos ábrázolása

Mint fent említettük, az FD-DEVS az SP-DEVS relaxációja. Ez azt jelenti, hogy az FD-DEVS az SP-DEVS vacsora osztálya. Megadnánk egy crosswalk fényvezérlő FD-DEVS modelljét, amelyet ebben a Wikipédiában az SP-DEVS-hez használnak . ahol = {? p}; = {! g: 0,! g: 1,! w: 0,! w: 1}; = {BG, BW, G, GR, R, W, D}; = BG, (BG) = 0,5, (BW) = 0,5, (G) = 30, (GR) = 30, (R) = 2, (W) = 26, (D) = 2; (G, pp) = (GR, 0), (s, pp) = (s, 0), ha s G; (BG) = (! G: 1, BW), (BW) = (! W: 0, G), (G) = ( , G), (GR) = (! G: 0, R), (R ) = (! w: 1, W), (W) = (! w: 0, D), (D) = (! g: 1, G); ${\ displaystyle M = <X, Y, S, s_ {0}, \ tau, \ delta _ {x}, \ delta _ {y}>}$${\ displaystyle X}$${\ displaystyle Y}$${\ displaystyle S}$${\ displaystyle s_ {0}}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ delta _ {x}}$${\ displaystyle \ neq}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ phi}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$${\ displaystyle \ delta _ {y}}$

Az FD-DEVS modellek viselkedése

3. ábra: Az A játékos eseményszegmense és állapota pályája

Az FD-DEVS a DEVS egyik alosztálya

Az FD-DEVS modell az a DEVS ahol ${\ displaystyle M = <X, Y, S, s_ {0}, \ tau, \ delta _ {x}, \ delta _ {y}>}$ ${\ displaystyle {\ mathcal {M}} = <X, Y, S ', s_ {0}', ta, \ delta _ {ext}, \ delta _ {int}, \ lambda>}$

• ${\ displaystyle X, Y}$a következőkkel megegyeznek .${\ displaystyle {\ mathcal {M}}}$${\ displaystyle M}$
• ${\ displaystyle S '= \ {(s, t_ {s}): s \ in S, t_ {s} \ in \ mathbb {T} ^ {\ infty} \}}$
• ${\ displaystyle s_ {0} '= (s_ {0}, \ tau (s_ {0}))}$
• Adott állapot , ${\ displaystyle (s, t_ {s}) \ in S '}$${\ displaystyle ta (s, t_ {s}) = t_ {s}.}$
• Adott állapot és bemeneti esemény ,${\ displaystyle (s, t_ {s}) \ in S '}$${\ displaystyle x \ in X}$

${\ displaystyle \ delta _ {ext} (s, t_ {s}, t_ {e}, x) = {\ begin {esetben} (s ', t_ {s} -t_ {e}) és {\ text { if}} \ delta _ {x} (s, x) = (s ', 0) \\ (s', \ tau (s ')) és {\ text {if}} \ delta _ {x} (s , x) = (s ', 1) \\\ end {esetek}}}$

• Adott állapot , ha${\ displaystyle (s, t_ {s}) \ in S '}$${\ displaystyle \ delta _ {int} (s, t_ {s}) = (s ', \ tau (s'))}$${\ displaystyle \ delta _ {y} (s) = (y, s ').}$
• Adott állapot , ha${\ displaystyle (s, t_ {s}) \ in S '}$${\ displaystyle \ lambda (s, t_ {s}) = y}$${\ displaystyle \ delta _ {y} (s) = (y, s ').}$

A DEVS viselkedésének részleteiről az olvasók az Atom DEVS viselkedése című cikkben olvashatnak

Az A pingpong játékos viselkedése

A 3. ábra az A játékos, aki az 1. ábrán bemutatott ping-pong játékot játszik, egy eseményszegmenst (fent) és a hozzá tartozó állapotpályát (alul) mutatja. A 3. ábrán az A játékos állapotát (állapot , élettartam, eltelt idő) = ( ), és a 3. ábra aljának vonalszakasza az eltelt idő értékét jelöli. Mivel az A lejátszó kezdeti állapota "Küldés" és élettartama 0,1 másodperc, a (Küldés, 0,1, ) magassága 0,1, ami a értéke . Miután megváltozott (Várjon, inf, 0), amikor a nullázza 0, az A játékos nem tudja, mikor lesz újra 0. Mivel azonban a B játékos 0,1 másodperccel később visszaküldi a labdát az A játékosnak, az A játékos a 0,2 időpontban tér vissza (Küldés, 0,1 0). Ettől kezdve, 0,1 másodperccel később, amikor az A játékos állapota (Küldés, 0,1, 0,1) lesz, az A játékos visszaküldi a labdát a B játékosnak és bekerül (Várjon, inf, 0). Így ezek a ciklikus állapotátmenetek, amelyek a „Küldés” és a „Várakozás” között előre-hátra mozognak, örökké fognak tartani. ${\ displaystyle s, t_ {s}, t_ {e}}$${\ displaystyle t_ {e}}$${\ displaystyle t_ {s}}$${\ displaystyle t_ {e}}$${\ displaystyle t_ {e}}$

4. ábra: Eseményszegmens és egy kenyérpirító állapotpályája

Kenyérpirító viselkedése

A 4. ábra a 2. ábrán bemutatott kétrésű kenyérpirító bal oldali résének eseményszegmensét (felső) és a hozzá tartozó állapotpályát (alul) mutatja. A 3. ábrához hasonlóan a bal rés állapotát is ( állapot, élettartam, eltelt idő) = ( ) a 4. ábrán. Mivel a kenyérpirító kezdeti állapota "I" és élettartama végtelen, a (Várjon, inf, ) magasságát meg lehet határozni bekövetkezik. A 4. ábra azt az esetet szemlélteti, amikor a „push” a 40 időpontban történik, és a kenyérpirító (T, 20, 0) értékre változik. Ettől kezdve, 20 másodperccel később, amikor az állapota megváltozik (T, 20, 20), a kenyérpirító visszatér (Wait, inf, 0) helyre, ahol nem tudjuk, mikor tér vissza a „Toast” -ra. A 4. ábra azt az esetet mutatja, amikor a „push” a 90 időpontban következik be, így a kenyérpirító bejut (T, 20,0). Figyelje meg, hogy annak ellenére, hogy valaki a 97-es pillanatban újra nyomja, az állapot (T, 20, 7) egyáltalán nem változik, mert (T,? Push) = (T, 1). ${\ displaystyle s, t_ {s}, t_ {e}}$${\ displaystyle t_ {e}}$${\ displaystyle \ delta _ {x}}$

Előnyök

5. ábra Kéthelyes kenyérpirító elérhetõségi grafikonja

Az időzóna-absztrakció alkalmazhatósága

A nem negatív, racionálisan értékelt élettartamoknak az a tulajdonsága, amelyet a bemeneti események megőrzhetnek vagy megváltoztathatnak, valamint véges számú állapot és esemény garantálja, hogy az FD-DEVS hálózatok viselkedése ekvivalens véges-csúcs elérhetőségi gráfként elvonható a az eltelt idők végtelen sok értéke a D. Dill professzor [Dill89] által bevezetett idő absztrakciós technikával . A [HZ06a] , [HZ07] dokumentumban egy algoritmust hoztak létre, amely egy véges-csúcs elérhetõségi grafikont (RG) generál .

Elérhetőségi grafikon

Az 5. ábra a két résű kenyérpirító elérhetőségi grafikonját mutatja, amely a 2. ábrán látható. Az elérhetőségi grafikonon minden csúcsnak megvan a maga különálló állapota és időzónája, amelyek és és között vannak . Például az 5. ábra (6) csomópontjánál a diszkrét állapotinformáció ((E, ), (T, 40)), és az időzóna az . Minden irányított ív megmutatja, hogyan változik a forráscsúcsa a célcsúcssá, a hozzá tartozó eseményekkel és egy visszaállító modellkészlettel együtt. Például a (6) - (5) átmeneti ívet a push1 esemény váltja ki . Ekkor az ív {1} halmaza az 1 eltelt idejét jelöli (vagyis 0-val állítja vissza, amikor a (6) - (5) átmenet bekövetkezik. Részletesebb információkért az olvasó a [HZ07] -re hivatkozhat . ${\ displaystyle t_ {e1}, t_ {e2}}$${\ displaystyle t_ {e1} -t_ {e2}}$${\ displaystyle \ infty}$${\ displaystyle 0 \ leq t_ {e1} \ leq 40,0 \ leq t_ {e2} \ leq 40, -20 \ leq t_ {e1} -t_ {21} \ leq 0}$${\ displaystyle t_ {e1}}$

A biztonság határozhatósága

Minőségi tulajdonságként az FD-DEVS hálózat biztonsága úgy határozható meg, hogy (1) előállítja az adott hálózat RG-jét, és (2) ellenőrzi, hogy elérhető-e néhány rossz állapot vagy sem [HZ06b] .

Az Élet eldönthetősége

Minőségi tulajdonságként az FD-DEVS hálózat életképessége úgy határozható meg, hogy (1) generáljuk az adott hálózat RG-jét, (2) RG- jéből , kernel irányított aciklikus gráfot (KDAG) generálunk, amelyben egy csúcs erősen kapcsolódik az összetevőhöz , és ( 3) annak ellenőrzése, hogy a KDAG csúcsa tartalmaz-e olyan állapotátmeneti ciklust, amely tartalmaz egy élettartam-halmazt [HZ06b] .

Hátrányok

Gyenge expresszivitás a nemdeterminizmus leírására

Azok a tulajdonságok, amelyek az FD-DEVS összes jellegzetes funkciója determinisztikusak, valahogyan korlátozásnak tekinthetők a nem determinisztikus viselkedésű rendszer modellezésére. Például, ha az 1. ábrán látható ping-pong játék egyik játékosának sztochasztikus élettartama „Küldés” állapotban van, az FD-DEVS nem képes hatékonyan rögzíteni a nem-determiniszt. ${\ displaystyle \ tau, \ delta _ {x}, \ delta _ {y}}$

Eszköz

Ellenőrzés céljából

Két nyílt forráskódú könyvtárakat Devs # írt C # a http://xsy-csharp.sourceforge.net/DEVSsharp/ és XSY írt Python át https://code.google.com/p/xsy/ , hogy a támogatás bizonyos elérhetőségi grafikonon alapuló ellenőrzési algoritmusok a biztonság és az életképesség megtalálásához.

Szimulációhoz XML-en keresztül

A DEVS szabványosításához, különösen az FDDEVS alkalmazásával, Dr. Saurabh Mittal és munkatársai együtt dolgoztak az FDDEVS XML formátumának meghatározásán. Egy cikket találunk a http://www.duniptechnologies.com/research/xfddevs/ címen . Ezt a szabványos XML formátumot használták az UML végrehajtásához [RCMZ09] .

Lábjegyzetek

Hivatkozások

• [Dill89] DL Dill, "A véges állapotú egyidejű rendszerek időzítési feltételezései és ellenőrzése", A véges állapotú rendszerek számítógépes ellenőrzési módszereiről szóló műhely anyagában, 197-212. Oldal, Grenoble, Franciaország, 1989
• [Hwang05] MH Hwang, "Az átkonfigurálható automatizálási rendszerek véges állapotú globális viselkedésének generálása: DEVS megközelítés", Proceedings of 2005 IEEE-CASE , Edmonton, Kanada, 2005. augusztus 1-2. (Elérhető itt : http: // moonho .hwang.googlepages.com / publications )
• [HZ06a] MH Hwang és Bernard Zeigler , „A Modular Verification Framework using Final and Deterministic DEVS”, Proceedings of 2006 DEVS Symposium , pp57-65, Huntsville, Alabama, USA, (Elérhető: http: //www.acims. arizona.edu )
• [HZ06b] MH Hwang és Bernard Zeigler , "A véges és determinisztikus DEVS hálózatok elérhető grafikonja", Proceedings of 2006 DEVS Symposium , pp48-56, Huntsville, Alabama, USA, (Elérhető a http: //www.acims oldalon. arizona.edu )
• [HZ07] MH Hwang és Bernard Zeigler , "Véges és determinisztikus fejlettség elérhetõségi grafikonja", IEEE Transaction on Automation Science and Engineering, 6. évfolyam, 2009. év 3. szám, 454–467. Oldal, http://ieeexplore.ieee .org / xpl / freeabs_all.jsp? isnumber = 5153598 & arnumber = 5071137 & count = 19 & index = 7
• [RCMZ09] José L. Risco-Martín, Jesús M. de la Cruz, Saurabh Mittal és Bernard Zeigler , "eUDEVS: Executable UML with DEVS Theory of Modeling and Simulation", SIMULATION, Transaction of the Society for Modeling and Simulation International , 85. évfolyam, 2009. november 11–12., 750–777. Oldal, http://sim.sagepub.com/content/85/11-12/750.short
• [ZKP00] Bernard Zeigler , Tag Gon Kim, Herbert Praehofer (2000). Modellezés és szimuláció elmélete (második kiadás). Academic Press, New York. ISBN 978-0-12-778455-7.CS1 maint: több név: szerzők listája ( link )