Formális módszerek
(Formal Methods)
- 1 óra előadás (kollokvium), 2 laboratoriumi gyakolat (aláírás)
- 3 kredit, tavaszi félév
Tantárgyleírás
A tárgy oktatásának célja (kialakítandó kompetenciák):
Napjaink informatikai rendszerei eddig soha nem látott komplexitást értek el, és ezzel együtt növekszik a megbízható működésük iránti igény is. Ezért egyre inkább előtérbe kerülnek azok a matematikai módszerek, melyek segítséget nyújtanak az informatikai rendszerek tervezésében és ellenőrzésében, meghatározó szerepet vállalva a kíván megbízhatóság elérésében.
A kurzus ezeket az úgynevezett formális módszereket kívánja bemutatni, ismertetve nemcsak a matematikai hátteret, hanem a használatukat megkönnyítő szoftver eszközöket is.
Tematika
A formális módszerek fogalma, szerepe és értékelés az informatikai rendszerek fejlesztésében és ellenőrzésében. Verifikáció és validáció. A formális módszerek áttekintése.
Alapszintű matematikai formalizmusok. Átmeneti rendszerek, címkézett átmeneti rendszerek, Kripke struktúrák, automaták, Büchi-automaták, időzített automaták, időzített automaták hálózatai.
Formális specifikáció. Temporális logikák, lineáris (LTL) és elágazó idejű logikák (CTL,CTL*), időzített logikák, üzenet idősor diagramok (MSC, LSC).
Modellellenőrzés. A modellellenőrzés alapfeladata és menete. Modellellenőrzési algoritmusok. Szimbolikus modellellenőrzés, bináris döntési diagrammok. Valószínűségi modellellenőrzés, korlátos modellellenőrzés. Modellellenőrző eszközök: SAL, Spin, UPPAAL.
Petri hálók. Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok, tulajdonság modellek, invariánsok, Petri hálók analízise, színezett Petri hálók, Petri háló szimulátorok, a CPN Tool.
Processzus algebrák. Processzus gráfok és termek. Viselkedési ekvivalenciák. Strukturális operációs szemantika. Konkurens rendszerek verifikációja processzus algebrákkal. Az LTSA eszköz.
Ajánlott irodalom
1. Pataricza A. (szerk): Formális módszerek az informatikában, 2. kiadás, Typotex, 2005.
2. Ésik Z., Gombás É., Németh L. Z.: Hardver és szoftver rendszerek verifikációja, Typotex Kiadó, 2011.
3. L. Aceto, A. Ingólfsdóttir, K. G. Larsen, J. Srba, Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2007.
4. A. Arnold: Finite Transition Systems: Semantics of Communicating Systems, Prentice-Hall International Series in Dynamics, Prentice-Hall, 1994.
5. Ch. Baier and J--P. Katoen, Principles of Model Checking, MIT Press, 2008.
6. G. Behrmann, A. David, K. G. Larsen: A Tutorial on Uppaal, in: Proc. SFM-RT'04, LNCS 3185, 2004
7. B. Berard, M. Bidiot, A. Finkel, F. Laorussinie, A. Petitt, L. Pterucci, Ph. Schnoebelen: Systems and Software Verification, Springer, 2001.
8. G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003
Szoftver eszközök
1. Spin, http://spinroot.com/
2. Uppaal, http://www.uppaal.org/
3. SAL, http://sal.csl.sri.com/
4. CPN Tools,http://cpntools.org/
5. LTSA, http://www.doc.ic.ac.uk/ltsa/
Tantárgy felelőse
Fülöp Zoltán, egyetemi tanár, DSc
