Izbor
Prikaz specifikacije v jeziku Promela v razvojnem okolju Eclipse
Razpisana: 28. 11. 2005
Dodeljena:
Zagovarjana:
Študent:
Raziskovalec: Aleksander Vreže, dr. Boštjan Vlaovič
Opis naloge:
| Vhod v orodje je model sistema, opisan v jeziku Promela. Promela je modelirni jezik, ki se uporablja za opis modelov asinhronih sistemov s sočasnostjo. Sintaktična in semantična pravila jezika so podobna kot pri programskem jeziku C, kljub temu pa obstajajo nekatere bistvene razlike. Promela, za razliko od jezika C, omogoča tvorjenje procesov, komunikacijo med procesi, nedeterministično izbiro itd., ne omogoča pa nekaterih funkcionalnosti, ki jih navadno omogočajo višjenivojski programski jeziki, npr. implementacije funkcij, ki vračajo vrednosti, uporabe kazalcev ipd. Razlog izhaja iz dejstva, da jezik Promela ni programski jezik, temveč modelirni jezik, ki je namenjen modeliranju sistemov s sočasnostjo na višjem t.i. abstraktnem nivoju. V primeru daljšega opisa modela sistema postane opis težje berljiv in nepregleden. V okviru tega diplomskega dela se bo implementiral vtič (plug-in), ki bo omogočal grafični prikaz modela sistema, ki bo v največji možni meri sledil standardu SDL'92. Dodatno je potrebno implementirati možnosti različnih predogledov in izvoz v različne formate datotek. |
Zaželjena znanja: C++, Java
Formalna verifikacija telekomunikacijskih sistemov
V okviru Laboratorija za mikroračunalniške sisteme se raziskovalno ukvarjamo s formalno verifikacijo telekomunikacijskih sistemov s poudarkom na verifikaciji protokolov. V okviru diplomskih, magistrskih in doktorskih del smo pod mentorstvom red. prof. dr. Zmaga Brezočnika in izr. prof. dr. Tatjane Kapus razvili več programskih orodij. Delo na tem področju ni nikoli v celoti zaključeno, zato vas vabimo, da s svojim diplomskim delom prispevate k uresničitvi zastavljenih ciljev.
Od kandidata se ne pričakuje znanje s področja formalne verifikacije, pričakuje pa se pozitiven odnos do dela in želja po osvajanju novih znanj s področja razvoja programske opreme. Delo bo orientirano aplikativno s končnim ciljem razvoja dela okolja za formalno verifikacijo protokolov v telekomunikacijah, ki bo uporabno tudi za industrijske potrebe. Po opravljenem diplomskem delu nudimo možnost nadaljevanja študija v okviru razpisanih tem za magistrski in doktorski študij. Možen je tudi dogovor o zaposlitvi v okviru programa mladi raziskovalci.
Razvojno delo bo potekalo v sodelovanju s podiplomskimi študenti in raziskovalci na zmogljivem 64-bitnem strežniku pod operacijskim sistemom Linux. Za razvojno okolje smo izbrali Eclipse, ki ...
Zainteresirani kandidati naj pošljejo e-sporočilo na naslov bostjan.vlaovic[AT]uni-mb.si ali pokličejo na telefon +386 2 220 7217 (dr. Boštjan Vlaovič).
