Bartha Tamás, Majzik István

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

Példák színezett Petri-háló modellekre

A színezett Petri-hálók működését és legfontosabb jellemzőit két további példán keresztül mutatjuk be. Első példánk az eddig tárgyalt egyszerű számláló továbbfejlesztéseként is felfogható. A 4.30. ábrán bemutatott CPN-háló lifteknek a hívógombok hatására bekövetkező mozgását modellezi. A modellben k darab lift n darab emelet között mozog (k és n a modell deklarációs részében rögzített konstansok; példánkban k=3 és n=5). A hívógombok explicit megjelenítése helyett csak a hívások tartalmát (az i. lift menjen fel/le a j. emeletre) ábrázoltuk. A modellt az összetartozó strukturális elemek színezésével igyekeztünk szemléletesebbé tenni; erre a CPN Tools lehetőséget ad, de az esztétikumon kívül a modell működésére nincs hatása.

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