SP-DEVS - SP-DEVS

Az SP-DEVS rövidítése az "Ütemezés-megőrző diszkrét eseményrendszer-specifikáció" egy formalizmus a diszkrét eseményrendszerek modellezéséhez és elemzéséhez, mind szimulációs, mind ellenőrzési módon. Az SP-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 SP-DEVS-t úgy fejlesztették ki, hogy támogassa hálózatainak ellenőrző elemzését azzal, hogy garantálja az eredeti hálózatok véges csúcs elérhetőségi gráfjának elérését, amely körülbelül 30 éve a DEVS formalizmusának nyitott problémája volt. Ahhoz, hogy hálózatainak ilyen elérhetőségi gráfját megkapja, az SP-DEVS-nek a következő három korlátozást vezették be:

1. az eseménykészletek és az állapotkészletek finomsága,
2. - egy állapot élettartama racionális szám vagy végtelenség szerint megtervezhető, és -
3. a belső ütemterv megóvása minden külső eseménytől.

Így, SP-DEVS egy alosztályát mind DEVS és FD-DEVS . Ez a három korlátozás azt eredményezi, hogy az SP-DEVS osztály összekapcsolás alatt zárva van, bár az államok száma véges. Ez a tulajdonság lehetővé teszi bizonyos kvalitatív tulajdonságok és kvantitatív tulajdonságok véges csúcsú grafikonon alapuló ellenőrzését, még SP-DEVS csatolt modellek esetén is.

Crosswalk vezérlő példa

rendszerkövetelmények

1. ábra. Crosswalk rendszer

2. ábra. A Crosswalk fényvezérlő SP-DEVS modellje

Fontoljuk meg a keresztező rendszert. Mivel a vörös fény (vagy nem sétáló fény) a zöld fénnyel (vagy sétáló lámpával) ellentétes módon viselkedik, az egyszerűség kedvéért csak két fényt veszünk figyelembe: egy zöld fény (G) és egy séta fény (W ); és egy nyomógombot, amint az az 1. ábrán látható. Két G és W fényt akarunk vezérelni egy időzítési korlátozással.

Két lámpa inicializálásához 0,5 másodpercig tart, amíg a G bekapcsol, és 0,5 másodperccel később, W kialszik. Ezután 30 másodpercenként előfordulhat, hogy G kikapcsol és W bekapcsol, ha valaki megnyomja a nyomógombot. Biztonsági okokból W két másodpercre vált, miután G kiszállt. 26 másodperccel később W kiszáll, majd két másodperccel később G visszatér. Ez a viselkedés megismétlődik.

Vezérlő tervezése

A fenti követelményeknek megfelelő vezérlő felépítéséhez egy bemeneti esemény „nyomógomb” (rövidítve? P) és négy kimeneti esemény „zöld-be” (! G: 1), „zöld-ki” (! G) 0), 'walk-on' (! W: 1) és 'walk-off (! W: 0), amelyeket parancsjelekként használnak a zöld és a walk fényre. A vezérlő állapotkészletének tekintjük a „booting-green” (BG), „booting-walk” (BW), „green-on” (G), „green-to-red” (GR), ” red-on '(R),' walk-on '(W),' késleltetés '(D). Tervezzük meg az állapotátmeneteket a 2. ábra szerint. Kezdetben a vezérlő BG-n indul, amelynek élettartama 0,5 másodperc. Az élettartam után ebben a pillanatban BW állapotba kerül, és létrehozza a „zöld-on” eseményt is. Miután 0,5 másodpercig a BW-n marad, G állapotba lép, amelynek élettartama 30 másodperc. A vezérlő továbbra is G-n marad, ha G-t G-ig hurkol, anélkül, hogy bármilyen kimeneti eseményt generálna, vagy mozoghat GR-állapotba, amikor megkapja a külsõ bemeneti eseményt? De a GR-n való tényleges tartózkodási idő a hátralévő idő a G-n keresztüli hurkoláshoz. GR-től az R állapotba mozog, amikor egy kimeneti eseményt generál! G: 0 és R állapota két másodpercig tart, majd W állapotba mozog a kimenettel esemény! w: 1. 26 másodperc múlva generálódik D állapotba!!: 0-val, és miután 2 másodpercig marad D-en, visszatér G-be a kimeneti eseménygel! G: 1.

Atomic SP-DEVS

Formai meghatározás

A keresztező lámpák fenti vezérlője atomi SP-DEVS modellezéssel modellezhető. Formálisan, egy atomi SP-DEVS egy 7- tuple

${\ 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 az idő, fejlett funkció , amely meghatározza az élettartama egy állam, ahol azoknak a nem-negatív számok racionális plusz végtelenig.${\ displaystyle \ mathbb {Q} _ {[0, \ infty]}}$
• ${\ displaystyle \ delta _ {x}: S \ idő X \ jobbra mutató nyíl S}$a külső átmeneti függvény , amely meghatározza, hogy egy bemeneti esemény megváltoztatja a rendszer állapotát.
• ${\ displaystyle \ delta _ {y}: S \ jobbra mutató nyíl Y ^ {\ phi} \ alkalommal S}$a kimeneti és a belső átmeneti függvény , ahol és jelöli a csendes eseményt . A kimeneti és a belső átmeneti funkció meghatározza, hogy az állapot hogyan generálja a kimeneti eseményt, miközben az állapot belsőleg változik.${\ displaystyle Y ^ {\ phi} = Y \ cup \ {\ phi \}}$${\ displaystyle \ phi \ notin Y}$

A Crosswalk Controller hivatalos képviselete

A fenti 2. ábrán látható vezérlő írható, 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, p) = GR, (s, p) = s, 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 SP-DEVS modell viselkedése

3. ábra. Az SP-DEVS modell eseményszegmense és állapota

Az atomi SP-DEVS dinamikájának megragadásához be kell vezetnünk két, az időhöz kapcsolódó változót. Az egyik az élettartam , a másik az utolsó visszaállítás óta eltelt idő . Legyen az élettartam, amely nem folyamatosan növekszik, hanem beállítódik, amikor egy különálló esemény történik. Hagyja jelöli az eltelt időt, amely folyamatosan növeli az idő múlásával, ha nincs visszaállítást. ${\ displaystyle t_ {s} \ in \ mathbb {Q} _ {[0, \ infty]}}$${\ displaystyle t_ {e} \ in [0, \ infty]}$

3. ábra. ábra: a 2. ábrán látható SP-DEVS modell eseményszegmenséhez kapcsolódó állapotpálya. olyan eseménypályát mutat, amelyben a vízszintes tengely egy időtengely, tehát azt mutatja, hogy egy esemény egy adott időpontban fordul elő, például:! g: 1 fordul elő 0,5 és! w: 0 1,0 időegységnél, és így tovább. A 3. ábra alján látható a fenti eseményszegmenshez tartozó állapotpálya, amelyben az állapot élettartamához és az eltelt időhöz kapcsolódik . Például (G, 30, 11) azt jelzi, hogy az állapot G, élettartama és az eltelt idő 11 időegység. A 3. ábra fenékének szegmensei az eltelt idő időáramát mutatják, amely az egyetlen folyamatos változó az SP-DEVS-ben. ${\ displaystyle s \ in S}$${\ displaystyle (s, t_ {s}, t_ {e})}$

Az SF-DEVS egyik érdekes tulajdonsága lehet az SP-DEVS korlátozásának (3) ütemezésének megőrzése, amelyet a 3. ábra 47. időpontjában rajzolnak, amikor a külső esemény p történik. Ebben a pillanatban, annak ellenére, hogy az állapot G-ről GR-re változhat, az eltelt idő nem változik, tehát a vonalszakasz nem szakad meg a 47-es időpontban, és felnövekedhet, és ebben a példában 30-ra növekszik . Az ütemtervnek a bemeneti eseményektől való megóvása és az idő előrehaladásának a negatív racionális számra való korlátozása miatt (lásd a fenti (2) korlátozást), minden fűrész magassága lehet egy negatív racionális szám vagy végtelenség (amint az a 3. ábra alján látható) SP-DEVS modellben. ${\ displaystyle t_ {e}}$${\ displaystyle t_ {e}}$

Az SP-DEVS a DEVS alosztálya

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

• ${\ displaystyle X, Y}$Az ugyanaz, mint azok .${\ displaystyle {\ matematikai {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 állam , ${\ displaystyle (s, t_ {s}) \ az S '} -ben$${\ displaystyle ta (s, t_ {s}) = t_ {s}.}$
• Adott állapot és bemeneti esemény${\ displaystyle (s, t_ {s}) \ az S '} -ben$${\ displaystyle x \ X-ben, \ delta _ {ext} (s, t_ {s}, t_ {e}, x) = (s ', t_ {s} -t_ {e}) {\ text {if} } \ delta _ {x} (s, x) = s '.}$
• Adott állam , ha${\ displaystyle (s, t_ {s}) \ az S '} -ben$${\ displaystyle \ delta _ {int} (s, t_ {s}) = (s ', \ tau (s')}$${\ displaystyle \ delta _ {y} (s) = (y, s ').}$
• Adott állam , ha${\ displaystyle (s, t_ {s}) \ az S '} -ben$${\ displaystyle \ lambda (s, t_ {s}) = y}$${\ displaystyle \ delta _ {y} (s) = (y, s ').}$

Előnyök

• Az idővonal-absztrakció alkalmazhatósága

A nem negatív, ésszerűen értékelt élettartamok tulajdonságai, amelyeket nem változtatnak meg a bemeneti események, valamint a véges államok és események száma, garantálják, hogy az SP-DEVS hálózatok viselkedése egyenértékű véges csúcsú elérhetőségi gráfként vonható ki a végtelen absztrakcióval. a kidolgozott idők sok értéke.

Absztrakt végtelenül-sok esetben az eltelt idő az egyes komponensek SP-DEVS hálózatok egy idő-kivételi módszer, az úgynevezett time-vonal kivételi került bevezetésre [Hwang05] , [HCZF07] , amelyben a megrendelések és relatív különbség a menetrendek megőrzik. Idővonal-absztrakciós technika alkalmazásával bármely SP-DEVS-hálózat viselkedése elérhetőségi gráfként vonható le, amelynek csúcsainak és éleinek száma véges.

• A biztonság dönthetősége

Minőségi tulajdonságként egy SP-DEVS hálózat biztonságát úgy dönthetjük el, hogy (1) elkészítjük az adott hálózat véges csúcs elérhetõségi gráfját és (2) megvizsgáljuk, hogy egyes rossz állapotok elérhetõk-e vagy sem [Hwang05] .

• Az életképesség dönthetősége

Minőségi tulajdonságként az SP-DEVS hálózat életképessége úgy dönthető el, hogy (1) az adott hálózat véges csúcs elérhetőségi gráfját (RG) generálja az RG-ből, (2) generál egy kernel- irányított aciklusos gráfot (KDAG), amelyben egy A csúcs szorosan összekapcsolt összetevő , és (3) annak ellenőrzése, hogy a KDAG csúcsa tartalmaz-e olyan állapotátmeneti ciklust, amely az élési állapotok halmazát tartalmazza [Hwang05] .

• A minimális / maximális feldolgozási időkorlátok eldönthetősége

Kvantitatív tulajdonságként az SP-DEVS hálózatok két eseményéből származó minimális és maximális feldolgozási időkorlátot kiszámolhatjuk (1) a véges csúcs elérhetőségi gráfjának elkészítésével és (2.a) úgy, hogy megtaláljuk a minimális feldolgozási idő legrövidebb útvonalait. és (2.b) a leghosszabb útvonalak megkeresésével (ha rendelkezésre állnak) a maximális feldolgozási időhöz [HCZF07] .

hátrányok

• Kevésbé kifejezőképesség: OPNA probléma

Legyen passzív az SP-DEVS modell teljes állapota , ha ; egyébként aktív . ${\ displaystyle (s, t_ {s}, t_ {e})}$${\ displaystyle t_ {s} = \ infty}$

Az SP-DEVS ismert korlátozása az a jelenség, hogy "ha egy SP-DEVS modell passzívvá válik, soha nem tér vissza aktívvá (OPNA)". Ezt a jelenséget először a [Hwang 05b] -ben találták meg, bár eredetileg ODNR-nek hívták ("ha egyszer meghal, soha nem tér vissza"). Ennek oka a fenti (3) korlátozás, amely szerint egyetlen bemeneti esemény sem változtathatja meg az ütemezést, így a passzív állapot nem váltható fel aktív állapotba.

Például a 3. ábra (b) ábra szerinti kenyérpirító modellek nem SP-DEVS, mivel az (I) alapjárathoz társított teljes állapot passzív, de aktív állapotba, "pirítósba" (T) mozog, amelynek pirulása az idő 20 másodperc vagy 40 másodperc. Valójában a 3. ábra (b) ábra szerinti modell FD-DEVS .

Eszköz

Van egy nyílt forráskódú könyvtár, a DEVS # néven a http://xsy-csharp.sourceforge.net/DEVSsharp/ , amely támogatja a biztonságosság és az életképesség megállapítására szolgáló néhány algoritmust, valamint a Min / Max feldolgozási időkorlátokat.

Lábjegyzetek

Irodalom

• [Hwang05] MH Hwang, "Oktatóanyag: Valósidejű rendszer ellenőrzése az ütemezés szerint megőrzött DEVS-ek alapján", a DEVS 2005. évi szimpóziumának folyóiratai, San Diego, 2005. április 2-8., ISBN  978-1-56555-293-7 (Elérhető a http://moonho.hwang.googlepages.com/publications címen )
• [Hwang05b] 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", 2005. IEEE-CASE folyóirat , Edmonton, Kanada, 2005. augusztus 1–2. (Elérhető a http: //moonho.hwang .googlepages.com / kiadványok )
• [HCZF07] MH Hwang, SK Cho, Bernard Zeigler és F. Lin, "Az ütemezésmegőrző DEVS időbeli korlátainak feldolgozása", ACIMS műszaki jelentés, 2007, (elérhető a http://www.acims.arizona.edu és http : //moonho.hwang.googlepages.com/publications )
• [Sedgewick02], R. Sedgewick, Algoritmusok a C ++-ban, 5. rész grafikus algoritmus , Addison Wesley, Boston, harmadik kiadás
• [ZKP00] Bernard Zeigler , Tag Gon Kim, Herbert Praehofer (2000). A modellezés és a 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 )