Bartha Tamás, Majzik István

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


Élő tulajdonság

Mérnöki rendszerekben az egyik legfontosabb jellemző a megbízhatóság, azaz a folyamatos működésre való képesség, aminek egyik gyakori veszélyeztető tényezője a tervezés során elkövetett hiba miatt a rendszerben maradt holtpont létezése. A holtpont (angolul deadlock) a rendszer olyan állapota, amelyből nem tud továbblépni, azaz képtelenné válik bármilyen tevékenység végrehajtására. Ezért a holtpontmentesség a Petri-háló modellek egyik legfontosabb vizsgált és megkívánt tulajdonsága. Egy N,M0 Petri-hálót holtpontmentesnek nevezünk, ha minden MiRN,M0 elérhető állapotában van legalább egy engedélyezett és tüzelhető tranzíció tk:Mi[tk>Mj, azaz a háló bármely Mi állapotából képes továbblépni egy Mj követő állapotba. A holtpont megfelelője az elérhetőségi gráfban egy olyan csomópont, amelyhez nem illeszkedik kifelé mutató él. Holtpontra láttunk példát a 4.13. ábrán (b) bemutatott elérhetőségi gráf M4 állapotában.

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