Formális módszerek

A tantárgy angol neve: Formal Methods

Adatlap utolsó módosítása: 2007. június 14.

Tantárgy lejárati dátuma: 2015. január 31.

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

Műszaki Informatika Szak

Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
VIMM3245 6 4/0/0/v 5 1/1
3. A tantárgyfelelős személy és tanszék Dr. Pataricza András,
A tantárgy tanszéki weboldala https://wiki.inf.mit.bme.hu/twiki/bin/view/Form/WebHome
4. A tantárgy előadója

Név:

Beosztás:

Tanszék, Int.:

dr. Pataricza András

egyetemi docens

MIT

dr. Bartha Tamás
egyetemi adjunktus
MIT
5. A tantárgy az alábbi témakörök ismeretére épít

Számítógép architektúrák, Digitális technika, Algoritmuselmélet, Számítógép hálózatok

6. Előtanulmányi rend
Kötelező:
((TárgyEredmény( "BMEVIMA2230" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMEVIMA2229" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMETE911708" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMEVIDH0930" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMEVIDH2207" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMEVIMA2607" , "jegy" , _ ) >= 2
VAGY (TárgyEredmény( "BMETE911708" , "jegy" , _ ) >= 2
VAGY TárgyEredmény( "BMEVIMAF509" , "jegy" , _ ) >= 2)
ÉS (TárgyEredmény( "BMEVIMAF509" , "felvétel" , _ ) >0)
VAGY TárgyEredmény( "BMEVIMA2207" , "felvétel" , _ ) >0
VAGY TárgyEredmény( "BMEVIMA2607" , "felvétel" , _ ) >0))

VAGY Szakirány2R( "KIEG", "2004/05/1" ) >0
VAGY Szakirány2R( "KIEGI", "2005/06/1" ) >0
VAGY Szakirány( ahol a SzakirányKód = "KIEGI", ahol a Ciklus = "2006/07/1")
VAGY KépzésLétezik( ahol a KépzésKód = "5N-08S")
VAGY KépzésLétezik( ahol a KépzésKód = "5N-M8")

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

A kötelező előtanulmányi rend az adott szak honlapján és képzési programjában található.

Ajánlott:

nincs.

7. A tantárgy célkitűzése

Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis.

A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve.

A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi 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, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket.

Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.

8. A tantárgy részletes tematikája

Informatikai rendszerek minőségi analízise

A formális módszerek az informatikai rendszerek tervezésében, specifikáció, modellalkotás, verifikáció, modellellenőrzés, helyességbizonyítás.

Petri ­hálók

Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok, tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság, perzisztencia).

Petri ­hálok analízis módszerei

Elérhetőségi gráf, invariánsok, Martinez-Silva algoritmus. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Predikátumok, diagnosztikai problémák modellezése. Színezett, jól­formált Petri ­hálok (Design/CPN, WFN).

Diszkrét idejű szimuláció alapjai

Petri-háló szimulátorok felépítése, szolgáltatásai. Folyamat (workflow) modellek készítése és kiértékelése. Számítógépes kísérlettervezés alapjai.

Alkalmazások

Real-time, konkurrens és elosztott alkalmazások modellezése. Gyártásautomatizálás és ütemezés. Digitális hardware tervezés. Workflow menedzsment. Ágens technológia formális modelljei (P-gráfok).

Állapottérképek

Állapottérkép modellek felépítése, szerkezete, szintaktikája. Működés: UML és a STATEMATE szemantika. Tervezés állapottérkép alapján.

Temporális logikák

Osztályozás. Lineáris temporális logika (LTL­ kielégíthetőség és érvényesség). Elágazó idejű temporális logika (BTL). CTL és CTL* (érvényesség és kielégíthetőség, FairCTL). Alkalmazás konkurrens és biztonságkritikus rendszerekben. Formalizálás, komplexitás, BDD alapú reprezentáció. Műveletek ROBBD-ken.

Modellenőrzés főbb módszerei, a tableau módszer. Szimbolikus modellellenőrzés. A SAL modellellenőrző által biztosított eszközkészlet.

Processz algebrák

Konkurrens nyelvek alapjai (CSP, CCS). Speciális leíróeszközök (Ada-hálók, P-gráfok).

Adatfolyamhálók

Modellezés adatfolyam hálókkal, modellfinomítás, konzisztencia ellenőrzés finomítás után.

Alkalmazások verifikációja és validációja

Transzformáció bázisú modellverifikáció.

9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium)

Előadás.

10. Követelmények

a. A szorgalmi időszakban:

A félévvégi aláírás feltétele egy zárthelyi, továbbá egy, a tárgy anyagát felölelő konstruktív féléves házifeladat előírt színvonalú elkészítése és legalább elégséges szintű teljesítése.
b. A vizsgaidőszakban:
A hallgatók a tárgyból írásbeli vizsgát tesznek. A jegyhatáron lévő hallgatók számára opcionális szóbeli lehetőséget biztosítunk. Az érintett hallgatók névsorát az írásbeli eredmények kihirdetésekor tesszük közzé. A vizsgajegyben a zárthelyire és a házi feladatra kapott jegyek átlagát 10 %-os súllyal figyelembe vesszük.

c. Elővizsga: nincs.

11. Pótlási lehetőségek

A nagyzárthelyi a szorgalmi időszakban egy alkalommal, a vizsgaidőszak első 3 hetében még egy alkalommal, különeljárási díj ellenében, pótolható.

A házi feladatok határidőn túl nem adhatók be, pótlásuk a vizsgaidőszakban nem lehetséges.

12. Konzultációs lehetőségek A tárgyból a féléves házifeladat megoldásához kapcsolódóan a szorgalmi időszakban két alkalommal biztosítunk lehetőséget.
13. Jegyzet, tankönyv, felhasználható irodalom

[1] Pataricza (szerk): Formális módszerek az informatikában, 2. kiadás, Typotex, 2005.

[2] Reisig-Rozenberg: Lectures on Petri Nets Vols 1-2, Springer, 1999.

[3] Desel: Petrinetze, lineare Algebra und lineare Programmierung. Teubner 1998.

[4] Iyer-Tang: Experimental Analysis of Computer System Dependability.

14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
Kontakt óra 60
Félévközi készülés órákra 14
Felkészülés zárthelyire 20
Házi feladat elkészítése 32
Kijelölt írásos tananyag elsajátítása -
Vizsgafelkészülés 24
Összesen 150
15. A tantárgy tematikáját kidolgozta

Név:

Beosztás:

Tanszék, Int.:

dr. Pataricza András

egyetemi docens

MIT

dr. Majzik István

egyetemi adjunktus

MIT

dr. Csertán György

egyetemi adjunktus

MIT

dr. Bartha Tamás

egyetemi adjunktus

MIT

Huszerl Gábor

egyetemi adjunktus

MIT

dr. Varró Dániel

egyetemi adjunktus

MIT