Bartha Tamás, Majzik István

Biztonságra tervezés és biztonságigazolás formális módszerei


Kiegészítő helytranszformáció

A véges kapacitás modellezését ugyanakkor a modell megfelelő átalakításával (kiegészítő helyek felvételével és alkalmas kezdőállapot megválasztásával) a végtelen kapacitású szimpla Petri-hálók osztályán belül is meg lehet oldani. Az átalakítás alapgondolata (lásd 4.7. ábra) az, hogy minden egyes korlátozott Kp kapacitású p hely mellé felveszünk egy további, a korlátozott kapacitású hely még kihasználatlan kapacitását nyilvántartó p' kiegészítő helyet. Ezután a háló működését kiegészítő élekkel úgy kell módosítani, hogy az eredeti p helyen és a szabad kapacitást adminisztráló p' helyen lévő tokenek számának összege így minden állapotban a p hely kapacitásával egyezzen meg: j:mjp+mjp'=Kp.

Biztonságra tervezés és biztonságigazolás formális módszerei

Tartalomjegyzék


Kiadó: Akadémiai Kiadó

Online megjelenés éve: 2019

ISBN: 978 963 454 291 9

Jelen jegyzet a Budapesti Műszaki és Gazdaságtudományi Egyetem Közlekedésmérnöki és Járműmérnöki Kara Autonóm járműirányítási mérnök MSc mesterszak képzéséhez készült kiegészítő tananyagként. Az autonóm járművek a jövőben olyan mértékben alakítják át a közlekedéssel kapcsolatos társadalmi elvárásokat, és ennek kapcsán biztonságos működésükkel kapcsolatban olyan elvárások fogalmazódnak meg, hogy a jegyzetben ismertetett biztonságigazolási módszerek egyre jobban integrálódni fognak a járműmérnöki gyakorlatba. Jegyzetünk megalapozó tankönyvnek tekinthető a formális módszerek mérnöki alkalmazása területén: bevezet a legfontosabb formális leírási módok használatába, segít a rendszerek modellezésének megértésében és elsajátításában, és bemutatja a modellellenőrzés legfontosabb módszereit.

Hivatkozás: https://mersz.hu/bartha-majzik-biztonsagra-tervezes-es-biztonsagigazolas-formalis-modszerei//

BibTeXEndNoteMendeleyZotero

Kivonat
fullscreenclose
printsave