Bartha Tamás, Majzik István

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

Kripke-struktúrák

A Kripke-struktúra (angolul Kripke structure, röviden KS) mint formalizmus alapelemei az állapotok és a köztük lévő tranzíciók. A modellben az állapotok tulajdonságait tudjuk megadni, erre a célra állapotcímkéket használhatunk. Például egy közlekedési lámpa vezérlője esetén a ,,Piros”, ,,Sárga”, ,,Zöld”, ,,Villogó sárga” címkék segítségével adjuk meg, hogy egy adott állapotban milyen színű lámpa és hogyan világít. Ha egy állapotra több tulajdonság is jellemző, akkor több címkét is hozzárendelhetünk. Például ha az előbbi vezérlő egy adott állapotában a piros és a sárga lámpa is világít, akkor ahhoz az állapothoz a ,,Piros” és a ,,Sárga” címkéket is hozzárendeljük. Ezeket a címkéket – mivel az állapotok lokális, tovább nem bontható tulajdonságait adják meg – atomi kijelentéseknek is nevezzük. Az atomi kijelentések halmaza az alkalmazásra jellemző, ennek megfelelően nagyon sokféle lehet. Programok esetén hivatkozhatunk a változók értékeire (pl. ,,y=2”), algoritmusok esetén a számítás állapotára (pl. ,,Eredmény kész”, ,,Hiba történt”).

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