Bartha Tamás, Majzik István

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

Változók és típusok

Ahhoz, hogy az egyszerű állapotátmeneti formalizmusra építve kompakt, hatékony és jól áttekinthető modellek alkotására adjon lehetőséget, az Uppaal rendszer a színezett Petri-hálóknál már látott megoldáshoz folyamodott: bevezette a változók és a velük megfogalmazható kifejezések alkalmazását az időzített automata leírásában. A változók úgy használhatók, ahogyan azt a tradicionális programozási nyelveknél már megszoktuk: típussal rendelkeznek, felhasználás előtt deklarálni kell őket, adhatunk nekik kezdőértéket, kifejezéseket képezhetünk velük, és az értéküket kiolvashatjuk, megváltoztathatjuk. A változók értékét az állapotátmeneteket jelképező élekre írt kifejezésekben lehet felhasználni és/vagy módosítani. A változók lehetnek globálisak (minden automata ugyanúgy látja és manipulálhatja ezeket), vagy lokálisak (egy adott automatához tartoznak, csak annak kifejezéseiben használhatók fel, más automata nem férhet hozzájuk).

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