Bartha Tamás, Majzik István

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

LTL modellellenőrzés tablómódszerrel

A tabló megközelítésben az ellenőrizendő LTL-kifejezést részekre bontjuk az operátorai mentén, és a részkifejezések esetén megvizsgáljuk, hogy azok mikor lehetnek igazak. A részkifejezésekből épül fel a levezetési fa: ennek csomópontjai tehát tartalmazzák azokat a részkifejezéseket, amelyeket igazzá akarunk tenni, az ágait pedig felbontási szabályokkal képezzük az operátorok jelentése alapján. A levezetési fa építéséhez természetesen a modellre is szükség van (hiszen a modellből derül ki, hogy például egy X operátorral felírt részkifejezés teljesüléséhez milyen következő állapotokat tudunk figyelembe venni). Ennek megfelelően egy kifejezés felbontása mindig a modell adott állapotán értelmezett – ez kezdetben a kezdőállapot, később pedig a felbontási szabálynak megfelelően változik.

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