Login
 Forum
 
 
Thesis topic proposal
 
István Majzik
Hatékony modellellenőrzési technikák kidolgozása

THESIS TOPIC PROPOSAL

Institute: Budapest University of Technology and Economics
computer sciences
Doctoral School of Informatics

Thesis supervisor: István Majzik
Location of studies (in Hungarian): Méréstechnika és Információs Rendszerek Tanszék
Abbreviation of location of studies: MIT


Description of the research topic:

Az informatikai rendszerekben bennmaradó szoftver hibák kockázatának növekedésével mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes (hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés: formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, ezeken formális verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai. A formális verifikáció egyik legsikeresebb módszere a modellellenőrzés. Ennek során a tervezett rendszer állapotterén kimerítő módon történik temporális logikák segítségével formalizált tulajdonságok ellenőrzése. A modellellenőrzéshez az évek során számos technikát dolgoztak ki (pl. szimbolikus modellellenőrzés, korlátos modellellenőrzés), ezek nagyméretű állapottereken is képesek a specifikált tulajdonságok vizsgálatára. A verifikáció gyorsabb és kisebb erőforrásigényű végrehajtása azonban még mindig jelentős kutatási feladat.
A doktori kutatás célja új technikák kidolgozása a modellellenőrzés hatékonyságának és használhatóságának növelésére. Ennek során meg kell vizsgálni és ki kell dolgozni az utóbbi években felmerült új ötletek és módszerek (szaturáció, tulajdonság-orientált ellenőrzések, állapottér redukció) integrált alkalmazását. Ugyancsak jelentős előrelépést ígér a korlátozott (az állapotér meghatározott részén végezhető) absztrakció módszerének kidolgozása. A tulajdonságok szempontjából elvárás mind lineáris, mind pedig elágazó idejű temporális logikák támogatása. A modellellenőrzés így adódó új algoritmusait úgy kell kiterjeszteni, hogy a tulajdonság megsértése esetén alkalmasak legyenek a hibakeresést segítő ellenpélda generálására. Szintén új megoldások szükségesek ahhoz, hogy az ellenpélda alapján automatikusan javaslatokat lehessen adni a modell módosítására.
A kutatás kapcsolódik az R5-COP nemzetközi kutatási projekthez valamint biztonságkritikus rendszerek fejlesztését célzó ipari projektekhez.

Number of students who can be accepted: 1

Deadline for application: 2015-01-05


2024. IV. 17.
ODT ülés
Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).

 
All rights reserved © 2007, Hungarian Doctoral Council. Doctoral Council registration number at commissioner for data protection: 02003/0001. Program version: 2.2358 ( 2017. X. 31. )