Bartha Tamás, Majzik István

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

Alapmodellek: automaták

Az időzített automaták alapját a címkézett állapotátmeneti rendszerek adják, amelyeket az alapszintű formális modellek között (3.1. fejezet) már bemutattunk. A modell állapotait tehát körök vagy ellipszisek, az állapotátmeneteket pedig irányított élek (nyilak) jelzik. Az állapotokat címkékkel láthatjuk el, amelyekre az ellenőrizni/bizonyítani kívánt tulajdonságok kifejezéseiben (specifikációjában) hivatkozhatunk. Az automatának egy időben csak egy állapota lehet aktív. Ez a működés indításakor a kezdőállapot, amelyet az Uppaal modellezési formalizmusában dupla körvonal jelez. A továbbiakban pedig az egymásra következő aktív állapotokat az állapotátmenetek tüzelése jelöli ki. Az az állapotátmenet tüzelhet, amelyik az aktuális aktív állapotból indul ki. Ha egy aktív állapotból több átmenet is indul, akkor a következő állapot kiválasztása véletlenszerű (nem determinisztikus) lesz. Az állapotátmenetekhez szintén rendelhetünk kiegészítő ,,szöveges mezőket”, ezek azonban nem hivatkozható címkék, hanem olyan kiértékelhető kifejezések, amelyek a modell működésének befolyásolására szolgálnak (pl. őrfeltételek vagy mellékhatással rendelkező akciók).

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