Bartha Tamás, Majzik István

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

Jól formált Petri-hálók

Láthattuk, hogy a színezett Petri-háló modellek rugalmasságát és széles körű alkalmazhatóságát a beépített ML funkcionális programozási nyelv és annak CPN ML kiterjesztései adják. Ugyanakkor éppen ezek akadályozzák meg a hatékony analízismódszerek (pl. a szimbolikus modellellenőrzés) kifejlesztését ehhez a hálótípushoz. Ezért a CPN-hálók megjelenése után rövidesen felmerült az igény olyan magas szintű Petri-háló formalizmus kidolgozására, amely a színhalmazok és az élkifejezések eszközkészletének korlátozása árán algoritmusok kidolgozását teszi lehetővé a folyamok, az állapottér-redukciók és az úgynevezett szimbolikus elérhetőségi gráf (Symbolic Reachability Graph, SRG) kiszámítására. Az SRG lehetővé teszi az állapottér kompakt ábrázolását azzal, hogy meghatározza az elérhető konkrét állapotok ekvivalens osztályait. Ezt eredetileg a strukturálisan egyenértékű objektumoknak (tokeneknek) a modellező általi előzetes meghatározása tette lehetővé, de később kidolgoztak egy módszert ezeknek magából a modellből való, automatikus levezetésére.

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

Műszaki tudományok BME KJK könyvek

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//

BibTeX EndNote Mendeley Zotero