Bartha Tamás, Majzik István

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


Modellellenőrzés

A modellellenőrzésről mint a formális verifikáció (más szóval a működés helyességének formális módszerekkel történő ellenőrzése/igazolása) egyik alapmódszeréről jegyzetünk részletesen ír az 5.2. fejezettől kezdődően. Itt az ellenőrizendő modellek a korábban (3.1. fejezet) megismert Kripke-struktúra vagy tranzíciós rendszer formájában adottak. Hogyan alkalmazható a modellellenőrzés Petri-háló alapú modellek vizsgálatára? A válasz triviális, ha a Petri-hálók elérhetőségi gráfjának és állapotterének kapcsolatára gondolunk: az elérhetőségi gráf a Petri-háló modell állapottere, ugyanakkor egy Kripke tranzíciós rendszerként is felfogható, amelyben az állapotokat a hozzájuk tartozó tokeneloszlás-vektorral címkézzük, az állapotátmeneteket pedig az ezeket kiváltó tüzelő tranzíciókkal. Így a Petri-háló modell verifikációját visszavezettük a háló elérhetőségi gráfjának mint Kripke tranzíciós rendszernek a modellellenőrzésére. Az ellenőrizendő tulajdonságokat pedig olyan temporális logikai kifejezésekkel tudjuk leírni, amelyek az állapotra (tehát a tokeneloszlás-vektor valamilyen jellemzőjére; pl. a helyen lévő tokenek száma) vagy az állapotátmenetre (pl. tranzíció tüzelhető) vonatkoznak.

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