Formális módszerek

A tantárgy angol neve: Formal Methods

Adatlap utolsó módosítása: 2010. január 15.

Budapesti Műszaki és Gazdaságtudományi Egyetem
Villamosmérnöki és Informatikai Kar

 Mérnök informatikus szak, MSc képzés

Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
VIMIM100 1 3/0/0/f 4  
3. A tantárgyfelelős személy és tanszék Dr. Majzik István,
A tantárgy tanszéki weboldala http://www.mit.bme.hu/oktatas/targyak/vimim100/
4. A tantárgy előadója

 Név:Beosztás: Tanszék: 
 dr. Majzik Istvánegyetemi docens MIT 
 dr. Bartha Tamásegyetemi docensMIT 
 Dr. Pataricza Andrásegyetemi tanárMIT 

5. A tantárgy az alábbi témakörök ismeretére épít -
6. Előtanulmányi rend
Kötelező:
NEM ( TárgyEredmény( "BMEVIMIMA07" , "jegy" , _ ) >= 2
VAGY
TárgyEredmény("BMEVIMIMA07", "FELVETEL", AktualisFelev()) > 0)

A fenti forma a Neptun sajátja, ezen technikai okokból nem változtattunk.

A kötelező előtanulmányi rendek grafikus formában itt láthatók.

Ajánlott:
-
7. A tantárgy célkitűzése

Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább követelmény az, hogy a kritikus komponensek megvalósítása bizonyítottan helyes legyen. Ennek egyik jellegzetes megoldása a formális modelleken alapuló tervezés és megvalósítás: A formális modellek analízisével vizsgálhatóvá válnak a tervezői döntések, bizonyíthatóak egyes tulajdonságok, valamint automatizálható a kódszintézis. A tárgy áttekintést ad az informatikai rendszerek formális modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a legfontosabb matematikai leíró paradigmákat, a modellezési nyelveket, valamint a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Demonstrálja ezek alkalmazását a rendszerszintű modellezés, a hardver tervezés, valamint a szoftver helyességbizonyítás és szintézis területén.

A tantárgy követelményeit eredményesen teljesítő hallgatók

  • megismerik és alkalmazni tudják a különböző formális módszereket és technológiákat,
  • képesek lesznek nem-formális rendszer leírások alapján matematikai modellt alkotni,
  • megismerik a különböző helyességbizonyítási technikák előnyeit és hátrányait,
  • tisztában lesznek a formális módszereket támogató alapvető eszközökkel.
8. A tantárgy részletes tematikája
  • Informatikai rendszerek formális modellezése és analízise (a tantárgy összefoglaló bevezetése): A formális módszerek szerepe az informatikai rendszerek tervezésében: követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás). Mérnöki és formális modellek kapcsolata, modell-transzformációk.
  • Alapszintű formális modellek és szemantikák: Kripke-struktúrák, tranzíciós rendszerek, időzített automaták, automaták hálózata.
  • Követelmények formalizálása temporális logikákkal: Lineáris temporális logika (LTL). Elágazó idejű temporális logikák (CTL, CTL*). Gyakorlati példák és alkalmazások (PSL).
  • Formális verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint szimbolikus technikákkal. Bináris döntési diagramok használata. Korlátos modell ellenőrzés. Gyakorlati alkalmazások: Egyszerű algoritmusok helyességének verifikálása (UPPAAL), tesztgenerálás modell ellenőrzővel.
  • Informatikai rendszerek dinamikus viselkedésének modellezése állapottérképekkel: Állapottérképek szintaktikája és szemantikája. Tervezés állapottérképek alapján. Gyakorlati alkalmazások: UML állapottérképek, szoftver forráskód generálás, biztonságkritikus rendszerek tervezése (SCADE).
  • Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság). Elérhetőségi gráf, invariánsok. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Színezett Petri hálók. Gyakorlati alkalmazások: Adatbázis kezelő konzisztencia vizsgálata, protokoll analízis.
  • Modellezés adatfolyam hálókkal: Adatfolyam hálók szintaktikája és szemantikája. Modellfinomítás, a finomítás konzisztenciájának ellenőrzése. Adatfolyam hálók alkalmazása üzleti folyamatok modellezésére és szolgáltatásbiztonságának ellenőrzésére. Gyakorlati alkalmazások: IBM Business Modeller, SCADE.
  • Informatikai rendszerek mérnöki modellezése és analízise: Metamodellezés, modelltranszformációk. Mintapéldák UML modellek formális verifikációjára.
9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium)

Előadás.

10. Követelmények
  • A szorgalmi időszakban: A félévközi jegy megszerzésének követelménye két zárthelyi és egy házi feladat legalább elégséges szintű teljesítése. A házi feladat részei egy kisméretű információs rendszer modelljének elkészítése valamint az elvárt tulajdonságok modell alapú analízise. A házi feladat kiadására a 4. oktatási héten kerül sor, a beadásához kapcsolódó beszámolók, ill. bemutatók a 10. oktatási héttől ütemezhetők. A félévközi jegyet 35-35%-os súllyal a két zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozza meg.
  • A vizsgaidőszakban: -
11. Pótlási lehetőségek A szorgalmi időszakban bármelyik zárthelyi pótlására van lehetőség, de egy hallgató csak egy zárthelyit pótolhat. Egy sikertelen zárthelyi újbóli pótlására a pótlási időszakban is van lehetőség. Házi feladatok határidőn túl a pótlási héten adhatók be, a késedelmes beadás 20% pontlevonással jár.
12. Konzultációs lehetőségek

A házi feladattal kapcsolatban a félév során konzultációs lehetőséget biztosítunk.

13. Jegyzet, tankönyv, felhasználható irodalom
  1. Pataricza András (szerk.): Formális módszerek az informatikában. TypoTeX Kiadó, 2005.

Ajánlott irodalom:

  1. W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.
  2. D. Peled: Software Reliability Methods. Springer Verlag, 2001.
  3. E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 2000.
  4. G. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.
14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
Kontakt óra42
Félévközi készülés órákra10
Felkészülés zárthelyire40
Házi feladat elkészítése16
Kijelölt írásos tananyag elsajátítása12
Vizsgafelkészülés0
Összesen120
15. A tantárgy tematikáját kidolgozta
 Név:Beosztás:Tanszék: 
Dr. Pataricza Andrásegyetemi tanár MIT
dr. Majzik Istvánegyetemi docens MIT 
dr. Bartha Tamás egyetemi docensMIT 
dr. Varró Dániel egyetemi docensMIT