A formális módszerek vasúti alkalmazása nagy múltra tekint vissza, számos kutatás és publikáció született már e területen, az elméleti eredmények átültetése a napi gyakorlatba mégis várat magára. Ennek okai közt megtalálható egyrészt az a többlet munkaigény, amely a szükséges háttérismeretek elsajátításához és alkalmazásához szükséges, másrészt az a bizalmatlanság, ami az elkészült formális leírásokat és elemzéseket fogadja. Jelen írásunkban egy esettanulmányt vizsgálunk meg két jelentősen eltérő formális módszerrel, és e példákon keresztül szeretnénk bemutatni, hogy megfelelő építkezéssel jól használható modellek létrehozása is lehetséges.
Ennek érdekében a két különböző formalizmus segítségével végeztük el egy adott vasútbiztosítási feladat két eltérő szemléletmódú megközelítésének vizsgálatát. Az állomási biztosítóberendezések két elterjedten használt konstrukciós alapelvét (vágányutas és nyomvonal elvű) azonos helyszínrajzra képeztük le. A modellezést egyrészt Petri hálókkal a PetriDotNet, másrészt nemdeterminisztikus véges automatákkal az UPPAAL eszközben hajtottuk végre. A biztosítóberendezésekre vonatkozó informális követelmények formalizálásával végrehajtottuk a modellellenőrzést is a modelleken. Az elvégzett munka alapján összehasonlítottuk és értékeltük a két eszközt a vasúti biztosítóberendezésekkel kapcsolatos felhasználási lehetőségük szempontjából.
1. Formális módszerek
A formális módszerek olyan elsősorban az informatika területén használt matematikai (jellemzően diszkrét matematika és matematikai logika) alapú technikák, melyek a rendszer-, ezen belül mind a szoftver-, mind a hardverfejlesztés során alkalmazhatóak. [1] A formális modellek szintakszisa és szemantikája jól meghatározott, egyértelmű és teljes, azaz nem rendelkeznek félreérthető vagy nem definiált elemekkel. Ennek köszönhetően a formális specifikációs módszerek használata biztosítja az egyértelműséget, ellenőrizhetőséget és ezek mellett az automatikus feldolgozhatóságot is. Tehát a formális modellek és specifikációk révén történő együttműködés és információcsere a fejlesztési folyamat résztvevői között nem jelent újabb bizonytalanságot vagy félreértést, ellentétben a szöveges és ad hoc jelölésrendszereken alapuló elavult, de egyelőre elterjedt mérnöki gyakorlattal. A végrehajtható (szimulálható és futtatható működésű) modellek már készítésük korai fázisában tesztelhetőek. Megfelelő elemzőeszköz esetén lehetőség van modellellenőrzésre is, mely a formális modellek teljes körű, azaz kimerítő ellenőrzését teszi lehetővé. A hibák korai fejlesztési fázisban való felfedésével a költségek alacsonyan tarthatók. Ha lehetőség van automatikus kódgenerálásra, és minősített kódgenerátor állítja elő a kódot, akkor a modellre vonatkozó helyességbizonyítás (az ellenőrzött tulajdonságok terjedelmében) a kódra vonatkozó helyességbizonyításként is érvényes marad. A formális módszerek (modellezés és modellellenőrzés) alkalmazását a biztosítóberendezések fejlesztése során az EN 50128 és EN 50129 szabványok is HR-ként, azaz erősen ajánlottként jelölik. [2][3]
2. Modellezés
Kétrészes cikkünk első része a kiválasztott esettanulmány a vasúti területen is jól ismert és kedvelt Petri hálók segítségével történő modellezését és vizsgálatát mutatja be. A Petri hálók elméletének leírása a Vezetékek Világa 2014/1-es számában [4] olvasható. Részletes, angol nyelvű leírást [5] közöl.
A modellezés során törekedtünk az egyszerű (kiterjesztéseket kerülő) Petri hálók használatára, melynek elsődleges célja a modellek ellenőrizhetőségének biztosítása volt. Az esettanulmány komplexitása és az átláthatóság javítása érdekében hierarchikus Petri hálókat használtunk. A hierarchikus Petri hálók alkalmazásának célja kettős lehet. Egyrészt lehetőséget ad a logikailag, funkcionálisan stb. egy egységet képező hálórészek alhálókba szervezésére (top-down modellezési irány). Ugyanakkor a nagyobb rendszer is összeállítható az előre elkészített alhálókból (bottom-up modellezési irány). Az alhálók közötti kapcsolat megteremtése helyettesítő tranzíciókkal történik. Ezek a helyettesítő tranzíciók a magasabb szintű hálókban találhatóak, és elrejtik az alhálókban megvalósított funkcionalitást. Az alhálók a főhálótól függetlenül szerkeszthetők, ezáltal az adott szinten lévő komplexitás alacsonyan tartható. A Petri hálós modellezés a PetriDotNet programmal [6] támogatottan történt, ami a Petri hálók szerkesztésére, szimulációjára és analízisére szolgáló keretrendszer. A futtatható modellek letölthetők [7]-ről.
2.1. A modellezett biztosítóberendezésszerkesztési elvek áttekintése
A biztosítóberendezések konstrukciós felépítésük, ill. a vágányúti logika leképezése szerint két fő csoportba sorolhatók. Ezek a táblázatos (vagy koordináta) és a nyomvonal (vagy geografikus) elvek, előbbi tovább bontható vágányutas illetve kaszkád elvekre. A kaszkád elv nem képezte a vizsgálatok tárgyát.
A táblázatos elv legjellemzőbb megjelenései a vágányutas elvű biztosítóberendezések (pl. a mechanikus berendezések, Integra stb.). A beállítható vágányutakhoz kapcsolódóan a függőségek megvalósítása két táblázat – a menetterv és az elzárási terv – alapján történik. Előbbi adja meg a vágányutak közötti kizárásokat, utóbbi pedig vágányutanként a lezáráshoz szükséges elemek állását.
A nyomvonalas elv alkalmazásában (pl. Dominó-70) a vágányúti elemek önálló objektumokként jelennek meg, melyek a topológiának megfelelően kapcsolódnak össze egymással. A váltók elvárt állása nincs előre definiálva, azt a berendezés minden vágányút számára beállításkor határozza meg. Jellemzően a vágányút start- és célpontjának kijelölése után az elemek között útvonalkeresés indul. A keresés csúccsal szemben talált váltóknál szétágazik, gyök felől találtaknál „lenyesi” a másik ágat, ezzel kizárva az onnan érkező esetleges keresést. Az oldalvédelmet nyújtó elemek szintén a keresés során jelölődnek ki. A vágányúti kizárások megvalósítása is elemenként történik. Két vágányút kizárja egymást, ha egy vágányúti elemet közösen, vagy egy oldalvédelmi elemet eltérő állásban használnának fel.
2.2. A modellezéshez felhasznált topológia (állomásrészlet)
A biztosítóberendezési elvek modellezéséhez egy célszerű elrendezést választottunk (ld. 1. ábra). A cél egy olyan topológia meghatározása volt, amely több vágányúti elemből (legalább két váltó) épül fel, és ezáltal több vágányút beállítására is lehetőség biztosít. Így az esettanulmány során kellően összetett, de még jól kezelhető modelleket építhettünk. A helyszínrajz egy háromvágányos állomásrész kezdőponti (páros) váltókörzetét és a hozzá tartozó T2 jelű biztosított tolatásjelzőjét jeleníti meg. Az esettanulmány az „A” jelű nyílt vonal felől induló, a T2 tolatásjelző által biztosított, a három vágány egyikére beállítható tolatóvágányutakhoz kapcsolódó funkcionalitás modellezésére irányult. Az „A” jelű szakasz nem része a modellnek, csupán a csatlakozó vonal azonosítására szolgál.
2.3. A modellezett funkciók
A modellezendő funkciók lehatárolásának elsődleges célja az volt, hogy az egy vágányúthoz tartozó valamennyi alapvető működés a lehető legegyszerűbb formában megjelenjen a modellben. A modellezett funkciók:
- vágányút kiválasztása/kijelölése,
- váltók átállítása és lezárása, vágányszakaszok lezárása,
- vágányút lezárása,
- a lezárt vágányút kijelölésének törlése,
- jelző szabadra állítás,
- tolató szerelvény közlekedése,
- a vágányút oldódása, és lehetőség új vágányút beállítására.
Célul tűztük ki, hogy a négy modell azonos funkciókörrel rendelkezzen a két elv tulajdonságainak minél jobb megtartása mellett.
2.4. Elhanyagolások, korlátok
A kijelölt feladat, illetve a választott helyszínrajz alapján a következő egyszerűsítéseket, elhanyagolásokat tettük:
1. Nem használtunk időzítéseket a modellezés során. Bár erre mindkét eszköz (PetriDotNet és UPPAAL) használatával lehetőség lett volna, a modellek nem kezelik az időt, csak az egyes állapotokat vesszük figyelembe. (Például a váltó csak a két végállásában lehet, ezek között a váltás pillanatszerű stb.) Ennek oka, hogy a vizsgálat középpontjában a folyamat állt, elegendő volt tehát az események bekövetkezését vagy be nem következését vizsgálni.
2. Csak egy irányba állíthatók be vágányutak: az „A” kezdőpont felől a három vágány egyikére. Az ellenkező irányba való közlekedést nem kezeli a modell. A vágányút célpontjait virtuális célokként képeztük le. Ez nem jelentősebb megszorítás a modellezendő rendszerrel kapcsolatban, mivel az ellenkező irány elhagyása nem jelent funkcióbeli elhagyást.
3. Az elrendezésből következően nincs lehetőség a megcsúszások kezelésére, így ezeket sem modelleztük.
4. Nem foglalkoztunk az oldalvédelmi kérdésekkel, az alapul vett helyszínrajzon nincsenek oldalvédelmet adni tudó elemek. A modellekben ez az elhanyagolás jelenti (a vágányúti működésre nézve) a legjelentősebb funkcióbeli korlátozást.
5. Az a döntés, hogy vonatmenet helyett tolatómenet beállítását modelleztük, hordozza azt az egyszerűsítést, hogy a vágányút lezárásához az elemek foglaltságát nem kell figyelembe venni. (A vágányút feloldásában, illetve a váltók állíthatósági feltételeinek vizsgálatában viszont szerepet játszanak a foglaltságok.)
6. Nem valósítottunk meg vágány úttárolási funkciót. Egyszerre csak egy vágányút jelölhető ki és állítható be annak érdekében, hogy a hozzá tartozó feltételek teljesülése jobban ellenőrizhető legyen (pl. „Ha a vonat elhaladt, akkor biztosan feloldódott minden elem?”). Új vágányút kijelölésére csak az előző teljes feloldódása után nyílik lehetőség.
7. Nem modelleztük az egyéni kezeléseket. A modellekben csak egyféle kezelés létezik, ez a start és cél (csatlakozó vonal és fogadóvágány) kijelölése. Minden működés a vágányút beállításához kötődik.
8. A vágányút lezárás és rögzítés funkciókat egy lépésben modelleztük, elhanyagoltunk bizonyos ellenőrzéseket. A valós berendezések egyes feltételek ellenőrzését a vágányút beállítás során többször elvégzik (pl. váltó végállás), illetve más feltételeket folyamatosan ellenőriznek (pl. a jelző szabadra állítását követően a jelző mögötti szakaszok foglaltságát).
9. Meghibásodással, hibás működéssel (pl. hamis foglaltság) sem számolnak a modellek, kizárólag a normál folyamat működését modelleztük.
10. A vágányút feloldásához a közlekedő vasúti járműveket a modellező eszközöknek megfelelően, kellően rövidnek tekintettük. Ez a feltétel működésbeli megszorítást a modellekre nézve nem jelent.
Valamennyi itt megemlített egyszerűsítés és elhanyagolás a későbbiekben feloldható, illetve a modellek ezek beépítésével tovább bővíthetők.
2.5. Vágányutas elv
A vágányutas elv modellezéséhez szükséges, a topológiának megfelelő menetterv az 1. táblázatban, az elzárási terv a 2. táblázatban látható. A modellekben a modellezett funkciók lefutása során a kezdőállapotból indulva először megtörténik a beállítandó vágányút véletlenszerű kiválasztása. Ekkor történik meg a menettervi függőségek ellenőrzése és beállítása is. A modellekben az állapotváltozások sorozata innentől az elzárási terv leképezésének megfelelően a beállítható három vágányút szerint ágazik szét. Ezeken az ágakon megtörténik a menetbeállítási parancsok kiadása, a váltók állítása és az egyes objektumok egyenkénti, majd a vágányút teljes lezáródása. A lezárást követően a T2 jelű tolatásjelző szabadra áll, és a tolatómenet leközlekedhet. A vágányút feloldását a váltókörzet után, a fogadóvágányokhoz tartozó oldószakaszok végzik. Ha az oldószakasz foglalt lett, majd felszabadult, ill. ezt követően a vágányút és az elemek lezárásai feloldódnak, akkor lehetőség van új menet beállítására.
2.6. Nyomvonalas elv
A nyomvonalas elv megvalósításához felépíthető az egyes vágányúti elemek kapcsolatrendszere, melyek között a kommunikáció zajlik, és melyek a hozzájuk rendelt vágányúti funkciókat önmagukban képesek ellátni. Az egyes objektumok neve az őket szimbolizáló téglalapokban látható a helyszínrajznak megfelelő elrendezésben (2. ábra).
A modellek működése a vágányutas modellekhez hasonlóan a start- és célpontok véletlenszerű kiválasztásával történik (ld. 3. ábra, az egyes funkciók színezése megegyezik a később alkalmazott színezésekkel). Ezután egy kijelölő lánc fut végig a startból a topológiának megfelelően összekapcsolt elemeken. A kijelölés a célba elérve visszafordul, és a folyamat lejátszódik a start irányába is. Ha egy váltó mindkét irányból megkapta a kijelölést, akkor a kívánt állásba állhat. Ha egy elem jól áll, és mindkét irányból ki van jelölve, lezáródhat. Ezután a kiválasztott célból a start felé végigfut a lezáró lánc.
Ha a vágányút le van zárva, akkor a kijelölésre már nincs szükség, így az eltörölhető. A kijelölés törlése szintén start→cél, majd cél→start irányban fut le. Ha vágányút kijelölés megszűnt, a T2 jelző szabadra állítható. Ekkor a tolatómenet a beállított vágányúton leközlekedhet. A menet a start felől indul és a célig haladva minden elemet érint, és egyenként feloldja őket. A vágányút teljes feloldása után új menet beállítására van lehetőség.
2.7. Vágányutas elv modellezése Petri hálóval a PetriDotNet eszközben
A menetterv és az elzárási terv függőségeit a főhálón egymás mellett helyeztük el, működésük egymás után következik (4. ábra).
A vágányút kijelölése a „honnan”-hely meghatározásával kezdődik, mely jelen példában csak az „A” irányú csatlakozó vonal lehet. Ehhez lehet ezután egy olyan „hová”-helyet választani, amibe a kiválasztott irányból beállított vágányúton el lehet jutni (ez esetben Vg. I-III.).
A vágányút meghatározásával („hová”- hely kiválasztása) kerülnek megvalósításra a menettervei függőségek. Ez a menettervi táblázat celláinak megfelelő, helyekből álló mátrixon történik. A tranzíció tüzelése során tokenek meglétét ellenőrizve bizonyosodik meg róla, hogy nincs kiválasztott kizáró menet, illetve tokenek elvételével letiltja az ellenséges meneteket. A kizárás a vágányút feloldásáig marad meg (ekkor kerülnek vissza a kiindulási állapotnak megfelelően a tokenek).
Ezt követően a modell az elzárási terv alapján három fő sorra oszlik, ami a három beállítandó vágányútnak megfelelő függőségeket tartalmazza. Egy vágányút lezáródása három lépcsőben történik. Először a vágányútban érintett váltók parancsot kapnak a megfelelő állásba való állításukra, melynek hatására szükség esetén átállnak. Ezután a vágányúti funkciókat végző hálórész a váltó elvárt állásának ellenőrzésével egyidejűleg lezárja azokat. A váltó lezárása után az érintett vágányszakaszok lezárása is egyesével megtörténik. Mikor minden vágányútban érintett elem lezáródott, létrejöhet a vágányút lezáródása, melyet vágányutanként külön tranzíció végez el. Tüzelése előtt ellenőriz valamennyi előfeltételt: a vágányútban részt vevő váltó(k) helyes (elvárt) végállását, valamint minden, a vágányútban érintett elem lezárt voltát. A tranzíciók működésükkel tokent juttatnak a vágányút lezáródását jelentő, valamint a jelző állítását lehetővé tevő helyekre. Az előbbi helyen lévő token egyben előkészíti a vágányút oldását (élesíti a fogadóvágányhoz tartozó oldószakaszt), utóbbi segítségével pedig szabadra áll a tolatásjelző.
Ezután a tolatómenet leközlekedhet, a jelzőt meghaladva a vágányutat végigjárja (a modellen nem jelenik meg), és rálép a megfelelő vágányon elhelyezett oldószakaszra. A foglalttá válással egy időben a jelző is átáll „Tilos a tolatás” állásba.A szakasz felszabadulásával egyszerre megtörténik a főháló (váltóállást kivéve) alapállapotba állítása:
- Feloldódik a vágányút.
- Feloldódnak a vágányúti elemek (váltók és vágányszakaszok).
- Megszűnik a váltók állására vonatkozó utasítás.
- A menettervi függőségek megszűnnek, újra token kerül a háló elején található helyekből álló mátrix megfelelő helyeire.
- Új vágányút válik kiválaszthatóvá.
Ezzel véget ér egy vágányút beállításának, felhasználásának és feloldásának folyamata, új vágányút beállítására van lehetőség.
A továbbiakban csak a teljes háló egy részének (2-es váltó) részletes bemutatásával foglalkozunk. A modell teljes leírását lásd [7]. A modellekben szereplő helyek és tranzíciók jelölése utal a leképezett vágányúti elemre, illetve az elvégzett funkcióra (pl.: „T_2KUAVg3” = tranzíció, ami a 2-es váltó kitérőbe állítására ad utasítást az „A” irányból a III. vágányra vezető vágány út beállításához. (Az elnevezések részletes leírását ld. [7])
Az 5. ábra a főháló (elzárási terv részének) a 2-es váltóra vonatkozó részletét mutatja. A főháló vágányutakhoz kapcsolódó hármas tagolása jól megfigyelhető. A különböző helyekhez szaggatott vonallal kapcsolódó „A2” jelű alháló külön képét a 6. ábra szemlélteti. A PetriDotNet eszközben kék színnel jelölt helyek az alhálók főhálóban is szereplő helyei.
A váltók állítására vonatkozó utasításokat kiadó („T_2KUAVg3”, „T_2EUAVg2” és „T_2EUAVg1”) tranzíciók tokent juttatnak a váltó egyenes („P_2EU”) vagy kitérő („P_2KU”) állásba állítására utasítást adó (vágányutaktól független) helyekre. Az első és a második vágányra beállítandó vágányutakhoz a 2-es váltó egyenes, a harmadik vágányra beállítandóéhoz pedig kitérő állására van szükség. A váltó elvárt állásának kijelölése egyértelmű, így az utasítás után a váltó átállhat („T_2AEK” vagy „T_2AKE” tüzelése, ld. 6. ábra). A váltó átállásának csak két feltétele van: kapja meg a megfelelő parancsot (token „P_2EU” vagy „P_2KU” helyen), és ne legyen lezárva (token „P_2LP” helyen). Mivel a modellben kiszigetelt szakaszként csak az oldószakaszok jelennek meg, a váltófoglaltság ellenőrzésére sem kerül sor. Foglalt váltó állítása természetesen nem megengedett, a példában ez úgy is értelmezhető, hogy a kezelő felelőssége meggyőződni a váltó szabad voltáról.
Ezután a főhálóban a váltó lezáró tranzíciók („T_2KLAVg3”, „T_2ELAVg2” és „T_2ELAVg1”) ellenőrzik a váltó elvárt végállását („P_2K” vagy „P_2E”), majd a „P_2LP” helyről elvéve és a „P_2L” helyre tokent juttatva elvégzik a lezárást.
2.8. Nyomvonalas elv modellezése Petri hálóval a PetriDotNet eszközben
A jobb áttekinthetőség érdekében ez a modell is fő- és alhálókból áll. A folyamatok lefutásának jobb követhetősége érdekében azonban nem minden objektum lett külön alhálóba szervezve, hanem csak az egyes funkciók. A felosztás a következőképp történt:
- Főháló: kijelölés, lezárás, kijelölés törlése
- Alháló 1: 2-es váltó állítás
- Alháló 2: 4-es váltó állítás
- Alháló 3: foglaltság és oldás
A főháló egyszerre több funkciót modellez, ezért több elérő hálórészből épül fel. Az egyes részek térbeli elrendezését a 7. ábra szemlélteti. A funkciók ilyen jellegű szintekbe szervezésének oka az volt, hogy az egyes horizontális hálórészek között vertikális, működésbeli kapcsolat van. A különböző funkciók, folyamatok az objektumokból és a helyszínrajznak megfelelő kapcsolataikból összeállított hálórészeken futnak le. Így összesen hat hálórész lett összeállítva a topológiának megfelelően (a 7. ábrán látható öt, illetve a külön alhálón megjelenő foglaltság és oldás). A start- és célpont kiválasztása egy egyedi hálórészen történik, a topológiától függetlenül.
A modell működése a főhálón kezdődik, előbb a startok, majd a célok közüli választással. (Jelen példában egy start van, „S1”.) A megfelelő tranzíciók tüzelése előkészíti a vágányút start/cél felőli kijelölését, valamint a kijelölés start/cél felőli törlését, a megfelelő helyekre juttatott token segítségével. Ezen tranzíció tüzelésével megkezdhető a vágányút kijelölése, mely csúccsal szemben érintett váltónál ketté ágazik, míg gyök felől érintetteknél levágja a másik ágon érkező kijelölés (keresés) lehetőségét. A keresés előbb a start felől, majd a kiválasztott cél irányából fut le.
Már a kijelölés során elkezdődik azon „oldalágak” kijelölésének törlése, melyek a vágányútban nem vesznek részt. Jelen topológián csak a start felől érkező kijelölés fog kettéágazni. Ha a kijelölés a startból olyan célhoz ér, amely nincs a vágányút céljaként kiválasztva, a hozzátartozó, a vágányútban már biztosan részt nem vevő oldalág kijelölése eltörölhető. Az elemek kijelölésének törlése addig tud visszafele haladni, amíg olyan elemhez nem ér, ami a vágányútban részt vesz. A kijelölés törlés folyamatának leírása a későbbiekben történik.
Amint egy elem mindkét részhálóban (mindkét irányból) kijelölésre kerül, lehetőség van az állítására és lezárására. A lezárás a kijelöléshez hasonlóan történik, a célpontok felől indulva. A célpontok cél felőli kijelölése indítja a folyamatot. Az egyes tranzíciók tüzelésükkel ellenőrzik, hogy az adott objektum ki van jelölve mind start és cél felől, és megfelelő állásban áll, illetve tokent juttatnak a lezárást jelentő helyre. A start és cél objektumok külön nem záródnak le. Feladatuk csak a kijelölés indítása, visszafele fordítása (célból a start felé), valamint a kijelölés törlésének előkészítése.
A lezáródás befejezését követően lehetőség lenne a vágányúthoz tartozó (tolatás) jelző állítására. Ezelőtt azonban el kell törölni a már beállított és lezáródott vágányút kijelölését. Ezzel biztosítjuk, hogy a kijelölés hálórész alapállapotába kerüljön, és ne maradjanak olyan felesleges tokenek, melyek szándékolatlan kijelöléshez vezetnének a későbbiekben. A kijelölés törlése is a start felől indul, annak ellenőrzésével, hogy a lezárás visszaért a startba. A start felől történő kijelölés törlésének folyamatát a vágányszakaszokhoz tartozó hálórészek mindkét irányból továbbadhatják, a váltókhoz tartozó hálórészek pedig bármely két irányból érkezőt a harmadik irányba továbbítják. A startból végigfutó kijelölés törlés nem ágazik szét, hanem csak a beállított vágányútnak megfelelő nyomvonalon fut le. Az egyes váltóktól viszont csak akkor halad tovább, ha az oldalágak kijelölésének törlése befejeződött.
Mivel csak egyetlen start kiválasztása lehetséges, a célból történő kijelölés törlése egyszerűbb hálórésszel rendelkezik. Ha a célból érkező kijelölés is „találkozna” csúccsal szemben fekvő váltóval, a hozzá tartozó oldalág is a fentihez hasonló bonyolultságú lenne. A célból csak a kiválasztott célnak megfelelő törlés indul el, és fut végig egyértelműen a csak gyök felől érintett váltókon.
Ha a kijelölés törlés visszaért a startba, a T2 jelző szabadra állítható. A jelző szabadra állása után a menet leközlekedhet a beállított vágányúton, mely során oldja a lezárást. A tolatómentet egy, az oldás hálón a beállított vágányútnak (váltók állásának) megfelelően végigfutó token jeleníti meg (egységnyi hosszúságúnak tekintett vasúti jármű). Egy lezárt elem oldásának feltételei (a vágányutat fedező jelző szabadra kapcsolásán és „Megállj!” állásba visszaállításán kívül):
- az előző foglaltsági szakasz foglalt volt (és az azonos működés következtében feloldódott),
- az éppen vizsgált szakasz foglalt lett,
- a következő szakasz foglalt lett,
- a vizsgált szakasz felszabadult.
A foglaltságot továbbadó tranzíció tüzelése elvégzi az adott elem feloldását is, a kijelölés törléshez hasonlóan a lezárás helyekről elvett tokennel. A tolatómenet közlekedésének feltétele, hogy a tolatásjelző továbbhaladást engedélyező jelzési képet mutasson. A tolatásjelző „Tilos a tolatás” állásba az első mögötte lévő szakasz (2-es váltó) foglalttá válását követő felszabadulásával egy időben kapcsolódik vissza. A vágányútoldás elindulásának tehát feltétele a jelző ismételten felvett továbbhaladást tiltó állása. Ha a foglaltsági alháló végfutott, és a lezárt vágányút feloldódott (minden háló a – váltóállást kivéve – alapállapotában van), új start- és célpontok kijelölésére nyílik lehetőség.
A továbbiakban részletesen bemutatjuk a 2-es váltó működését. A 8. ábrán az eddig alkalmazott funkció szerinti színezéssel ki vannak emelve a topológia alakját lekövető hálórészek, melyek az elemek nyomvonalas kapcsolatának felelnek meg.
A nyomvonalas elvű kijelölés úgy valósul meg, hogy a csúcs felől érkező keresés tranzícióban („T_KS2E”) ágazik el, illetve a gyök felől jövő keresések hely elemben találkoznak („T_KCS1_2”). Egy elem kijelölése úgy történik, hogy a kijelölést végző tranzíció a kijelölés továbbadása mellet az adott objektumhoz tartozó kijelölő „pót helyről” („P_KS2EP”) a tokent áthelyezi a kijelölő helyre („P_KS2E”). A gyök felől érkező kijelölésekhez egy közös „pót hely” tartozik, azáltal biztosított csak az egyik ág kijelölése mellett a másik ki nem jelölése („P_KC2P” valamint „P_KC2J” és P_KC2B”). A „pót helyek” különböző ellenőrzésekben vesznek részt bizonyos információk negáltjának előállításában (pl. a váltó nincs lezárva), illetve kapacitáskorlátként szolgálnak a célból, hogy egyes működések csak egyszer futhassanak le (pl. egy objektumot egy irányból csak egyszer lehessen kijelölni).
Kijelöléstől függően a váltók állítása lehet szükséges, melyet az „A2” alháló valósít meg (ld. 9. ábra). Egy váltó csak akkor állítható („T_2AJB” vagy „T_2ABJ” tüzelése), ha ki van jelölve az eleje (token a „P_KS2E” helyen) és valamelyik szára felől (token a „P_KC2J” vagy „P_KC2B” helyen), nincs lezárva (token a „P_L2P” helyen) és nem foglalt (token a „P_F2P” helyen). (A tranzíciók nevében az álláshoz tartozó betűk sorrendje az állításra utal, pl. „T_2AJB”: 2-es váltó állítás jobb végállásból bal végállásba.) Amennyiben a váltó állítása nem szükséges, egyből lezáródhat. Ellenkező esetben a fent leírt feltételek együttes teljesülése esetén a váltó átáll, és azután záródik le (a „P_L2P” helyről a token átkerül a „P_L2” helyre) a megfelelő végállás (token „P_2J” vagy „P_2B” helyen) ellenőrzése mellett.
2.9. Petri hálók tulajdonságának ellenőrzése
A Petri hálók nem csak modellellenőrzés segítségével vizsgálhatók, hanem lehetőség van definiált, a Petri hálókra jellemző explicit tulajdonságok (ezeket ld. bővebben [5]) ellenőrzésére. Ezek egy része jól ismert algoritmusokra vezethető vissza, melyet számos Petri hálót szerkesztőelemző eszközben megvalósítottak. Az elkészített modelleken a következő tulajdonságokat ellenőriztük a PetriDotNet eszköz felhasználásával:
- Holtpontmentesség: nem akadnak el a modellek, azaz nem kerülnek olyan (deadlock) állapotba, amelyből nem tudnak továbblépni.
- Korlátosság: az adott helyeken (és ezáltal a modellben összesen) a tokenek száma egy ismert felső határ alatt lehet. A bemutatott modellek e tulajdonság egy megszorítását, a biztosságot kell, hogy teljesítsék. Ennek értelmében minden helyen legfeljebb egy token lehet.
- Megfordíthatóság: annak vizsgálata, hogy bármely kezdőállapotból elérhető állapotból vissza lehet jutni a kezdőállapotba. Ennél egyszerűbb feltétel teljesítése is elegendő a modellek esetében, azaz létezik olyan visszatérő állapot, amelyben új vágányút kijelölése lehetséges.
A tulajdonságok teljesülését a PetriDotNet eszközben vizsgáltuk, melynek eredménye tulajdonság sértést nem tárt fel. Ezen felül a modelleken modellellenőrzést is alkalmaztunk, amit a következő részben ismertetünk.
Felhasznált irodalom
[1] ÉSIK Zoltán [et al.] Hardver- és szoftverrendszerek verifikációja. Szeged, Typotex, 2011., ISBN 978-963-279-497-6
[2] MSZ EN 50129 Railway applications – Communication, signaling and processing systems – Safety related electronic systems for signaling Budapest, MSZT, 2003
[3] MSZ EN 50128 Vasúti alkalmazások. Távközlési, biztosítóberendezési és adatfeldolgozó rendszerek. Szoftverek vasúti vezérlő- és védelmi rendszerekhez Budapest, MSZT, 2011
[4] CSEH Attila [et al.] Biztosítóberendezések modellezése Petri hálókkal Vezetékek Világa, 19. évf. 1. sz. (2014) pp. 14-17. ISSN 1416-1656
[5] MURATA, Tadao Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE. Vol. 77, No. 4. (1989) pp. 542-559.
[6] BME MIT PetriDotNet, URL: https://inf.mit.bme.hu/research/tools/petridotnet
[7] FARKAS Balázs Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén [diplomaterv] Budapest, BME, 2016 URL: http://www.kjit.bme.hu/index.php/hu/folap/17-kutatas/352-formalismodszerek-kutatocsoport
Farkas Balázs, Lukács Gábor, Dr. Bartha Tamás
A cikk a Vasúti VezetékVilág 2017. júniusi számában jelent meg.