• Znanost
 

Znanost

V okviru Laboratorija za mikroračunalniške sisteme se raziskovalno ukvarjamo s formalno verifikacijo telekomunikacijskih sistemov s poudarkom na verifikaciji protokolov.

Sodobna družba se vedno bolj zanaša na pravilno delovanje digitalnih naprav v vseh svojih aktivnostih. Vedno pogosteje je od pravilnega izvajanja predvidenih operacij odvisno tudi človeško življenje. Še posebno hitro se razvijata telekomunikacijska in računalniška industrija. V zadnjih letih dosežki ene neposredno vplivajo na razvoj druge. Stičišče obeh industrij predstavlja komunikacija med napravami.

Tržni mehanizmi narekujejo kratke razvojne roke za nove izdelke in nenehne izboljšave obstoječih sistemov. Sočasno s krajšimi razvojnimi roki raste kompleksnost operacij. Zaradi povečevanja funkcionalne kompleksnosti telekomunikacijskih sistemov postaja njihova specifikacija vedno težja, možnost napak v specifikaciji in izvedbi pa vedno večja. Zato je potrebno izbrati ustrezne metode, orodja in postopke, da se temu problemu v čim večji meri izognemo.

Tradicionalne metodologije razvoja programske opreme temeljijo na neformalnih tekstualnih opisih. Uporaba metodologij, ki ne temeljijo na formalnih metodah, omejuje možnost preverjanja pravilnosti delovanja specifikacij protokolov na testiranje. Iskanje napake je torej omejeno na preverjanje skladnosti s pripravljenimi testnimi zaporedji. Z večanjem kompleksnosti sistema se brez uporabe formalnih metod celovitost preverjanja sistema manjša.

Večina sodobnih protokolov je tako kompleksnih, da bi preverjanje vseh mogočih izvajalnih poti trajalo nesprejemljivo dolgo, v sistemih s sočasnostjo pa to pogosto tudi ni mogoče. S tem dopuščamo možnost, da nepravilnosti v sistemu spregledamo. V primeru, ko se napaka odkrije v tržno uspešnem izdelku, so stroški pogosto zelo visoki. Zato težimo k temu, da bi s sistematično uporabo formalih metod v čim večji meri zagotovili pravilno delovanje sistema.

Spekter uporabe formalnih metod zajema vse razvojne korake. Od natančnega zapisa specifikacije sistema pa vse do formalne verifikacije končne implementacije sistema. V zadnjih treh desetletjih se je na področju formalnih tehnik opisovanja sistemov izdelala množica različnih formalizmov in pristopov k obravnavi problematike.

V okviru 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 magistrskim delom ali doktorsko disertacijo prispevate k uresničitvi zastavljenih ciljev.

Od kandidata se ne pričakuje poglobljeno znanje s področja formalne verifikacije, pričakuje pa se pozitiven odnos do dela in želja po osvajanju novih znanj s tega področja.

Delo bo razdeljeno na teoretični in aplikativni del s končnim ciljem razvoja okolja za formalno verifikacijo protokolov v telekomunikacijah, ki bouporabno tudi za industrijske potrebe. Med izvajanjem raziskovalnega dela nudimo sodelovanje na aktualnih raziskovalnih projektih.

Razvojno delo bo potekalo v sodelovanju z ostalimi 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 ali pokličejo na telefon +386 2 220 7217 (doc. dr. Boštjan Vlaovič).