Thesis supervisor: Dániel Varró
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:
Napjainkban a modellvezérelt tervezési módszertan egyre növekvő térhódítása figyelhető meg a rendszertervezés területén. A modellvezérelt tervezést egy precíz modellezési fázis vezet be, amely során számos nézőpontból vizsgáljuk meg a tervezés alatt álló rendszert, majd az integrált rendszertervet precíz matematikai analízisnek vetjük alá automatikus modelltranszformációk által. A garantált minőségű rendszertervből kiindulva az alkalmazás forráskódját és a telepítési információt automatikus kódgenerálás segítségével származtatjuk, amelyet tipikusan szintén egy speciális modelltranszformációnak tekinthetünk
Automatikus modelltranszformációk alkalmazásakor azonban problémát jelent, hogy vajon mennyire megbízhatóak maguk a modelltranszformációk. A gráftranszformációk paradigmája egy intuitív és egyben precíz formális módszert ad e modelltranszformációk specifikációjára. Amennyiben a transzformációk specifikációi koncepcionális hibákat tartalmaznak, ezek megjelennek a modelltranszformációk végrehajtásakor is, így gyakorta maguk a modelltranszformációk jelentik a minőségi szűk keresztmetszetet. Ezt elkerülendő, egyre inkább elengedhetetlenné válik a modelltranszformációk formális helyességellenőrzése.
A modelltranszformációk helyességellenőrzése során egyrészt garantálni kell, hogy a célnyelv jólformáltsági kritériumai teljesülnek, valamint további, transzformáció-specifikus kritériumok helyességét is igazolnunk kell, általános esetben tetszőleges forrásmodellből kiindulva. Ehhez precíz absztrakciók segítségével elsőrendű logikai formulákat származtatunk, amelyet automatikus tételbizonyítók segítségével dolgozhatunk fel.
A jelölt által elvégzendő kutatómunka eredményeként elsődlegesen az alábbi területeken várható új tudományos eredmény:
- Modellezési nyelvek és transzformációik konzisztenciavizsgálata, melynek keretében a gráfminták által definiált származtatott attribútumokat, jólformáltsági kényszereket és absztrakciót végző modelltranszformációkat az elsőrendű logika hatékonyan analizálható résznyelvébe képezzük, majd helyességvizsgálatára SAT/SMT-megoldók felhasználásával végezhetjük.
- Absztrakciós modell-leképezések tanúsítványozása, amikor a gráfminták által definiált leképezések helyességét két (vagy több) alternatív (független) helyességellenőrzési technika együttes alkalmazásával igazoljuk
- Végtelen állapotterű transzformációs rendszerek analízise, ekkor a forma (shape) analízis módszerét felhasználva a gráf alapú modelleket ekvivalencia osztályokba soroljuk, és ezeket címkézett gráfok speciális halmazával, formákkal ábrázoljuk. A transzformációs lépések absztrakt megfelelőjét végigvezetve a formákon biztosan véges állapotteret kapunk, melynek analízisével bizonyíthatjuk a végtelen állapotterű transzformációs rendszer helyességét.
A doktori kiírás szorosan kötődik a CERTIMOT ERC_HU_09 kutatási projekthez és a brazil Embraer céggel közösen végzett kollaborációs projekthez.
A téma feldolgozásához elengedhetetlen az angol nyelv ismerete.
Required language skills: angol Number of students who can be accepted: 1
Deadline for application: 2014-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).
Login
