A tantárgyleírás hatályossága
Hatályosság kezdete:
2026. March 21.
Hatályosság vége:
—
| Subject name (Hungarian, English) |
Formális módszerek
Formal Methods
|
||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Subject code | BMEVIMIMA19 | ||||||||||||
| Subject type | — | ||||||||||||
| Training Level | — | ||||||||||||
| Course types and hours (weekly/semester) |
|
||||||||||||
| Assessment type | félévközi érdemjegy | ||||||||||||
| Credits | 3 | ||||||||||||
| Subject coordinator |
DR. Majzik István
position: egyetemi docens
contact:
majzik.istvan@vik.bme.hu
|
||||||||||||
| Responsible department |
Mesterséges Intelligencia és Rendszertervezés Tanszék
|
||||||||||||
| Faculty | Villamosmérnöki és Informatikai Kar | ||||||||||||
| Subject website | — | ||||||||||||
| Primary curriculum type | — | ||||||||||||
| Direct prerequisites – Strong prerequisite | none | ||||||||||||
| Direct prerequisites – Weak prerequisite | none | ||||||||||||
| Direct prerequisites – Parallel prerequisite | none | ||||||||||||
| Direct prerequisites – Milestone prerequisite | none | ||||||||||||
| Direct prerequisites – Exclusion | none |
Objectives
Programme
- 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 szimbolikus technikákkal. 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, Yakindu Statechart Tools.
- Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Dinamikus tulajdonságok (elérhetőség, korlátosság, megfordíthatóság, visszatérő állapotok, élő tulajdonság). Elérhetőségi gráf. Strukturális tulajdonságok (invariánsok). Redukciós technikák. Gyakorlati alkalmazások: protokoll analízis.
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. 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, valamint a szoftver helyességbizonyítás területén.
A tantárgy követelményeit
eredményesen teljesítő hallgatók
megismerik és alkalmazni tudnak egyes 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.
Learning outcomes
Ez a tantárgy a KKK rendeletben meghatározott, következő kompetenciák fejlesztését szolgálja:
Knowledge
No learning outcomes recorded.
Skills
No learning outcomes recorded.
Attitudes
No learning outcomes recorded.
Autonomy and responsibility
No learning outcomes recorded.
Oktatási módszertan
Előadás
Tanulástámogató anyagok
Not provided.
Recommended preliminary knowledge for completing the subject
Knowledge type competencies
(azon előzetes ismeretek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)
nincs
Skill type competencies
(azon előzetes képességek és készségek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)
nincs
Recommended (non-compulsory) preliminary competencies
(azon ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák összessége, amelyek jelentősen hozzájárulnak a tantárgy eredményes teljesítéséhez)
nincs
General rules
Követelmények:
A szorgalmi időszakban:
A félévközi jegy megszerzésének követelménye egy zárthelyi dolgozat é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 70%-os súllyal a zárthelyi osztályzata és 30%-os
súllyal a házi feladat osztályzata határozza meg.A vizsgaidőszakban: -
Pótlási lehetőségek:
A zárthelyi dolgozat egy alkalommal
a szorgalmi időszakban pótolható vagy javítható. Sikertelen zárthelyi pótlására
egy alkalommal a pótlási időszakban is van lehetőség. Házi feladatok határidőn
túl a pótlási időszakban adhatók be, a késedelmes beadás 20% pontlevonással
jár.
Assessment methods
In-term assessments
No detailed assessments provided.
Weight of in-term assessments
No weights provided.
Exam-period assessments
No detailed assessments provided.
Weight of exam elements
No weights provided.
Grade calculation
No grade thresholds provided.
Attendance requirements
No attendance requirements provided.
Rules for retake and resubmission
Not provided.
Short description
Not provided.
Detailed description
Not provided.
Recommended courses
Not provided.
Workload to complete the subject
No workload breakdown provided.
Validity of subject requirements
Requirements valid from:
—
Requirements valid until:
—
Curriculum placement
No curriculum placements recorded for this subject version.