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 | BMEVIMIM100 | ||||||||||||
| Subject type | — | ||||||||||||
| Training Level | — | ||||||||||||
| Course types and hours (weekly/semester) |
|
||||||||||||
| Assessment type | félévközi érdemjegy | ||||||||||||
| Credits | 4 | ||||||||||||
| 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
As the complexity of information systems and the costs of potential failures are increasing, it becomes more and more important to prove that the design of the critical system components is correct. One of the typical solutions for the challenge of provenly correct design is the application of formal methods. Mathematically precise modelling and analysis allow the early verification of design choices, the proof of correctness with respect to several requirements, and then the automated software or hardware synthesis. The subject provides an overview of the formal background needed for the elaboration and analysis of the formal models of IT systems and components: the modelling paradigms, the widely used formal modelling languages, and the analysis and simulation based verification techniques. The subject demonstrates the application of formal methods in the field of system-level modelling, software design, verification and synthesis.
No objectives provided.
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
Not provided.
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 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: -
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.
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.