Bartha Tamás, Majzik István

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


Modellezési koncepció

Egy időzített automata tehát alapvetően egy címkézett állapotátmeneti rendszer, amelyet órákkal és az általuk képviselt idő fogalmával egészítenek ki. Folytonos (sűrű) időmodellt alkalmaz, ahol az óra mint változó értéke egy valós szám. Egy rendszert több ilyen időzített automata hálózataként, azaz párhuzamos (szinkron) kompozíciójaként modellezhetünk, ahol az összes időzített automata óraváltozói szinkronban haladnak. A modell tovább bővíthető korlátozott értékkészletű diszkrét változókkal, amelyek konkrét értékei az automata állapotának részét képezik. Ezeket a változókat a programozási nyelvekhez hasonlóan lehet használni: olvashatók, írhatók és általános aritmetikai műveletekkel manipulálhatók. A rendszer állapotát tehát az automaták állapota, az óraváltozók és a diszkrét hozzárendelt változók értékei együtt határozzák meg. Minden automata tüzelhet egy élet (végrehajthat egy állapotátmenetet), vagy szinkronizálhat egy másik automatával (ekkor a szinkronizáló automaták mindegyike egyszerre hajtja végre a megfelelő állapotátmenetet), és ez az egyedi vagy szinkron állapotátmenet egy új rendszerállapotot eredményez.

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