OKOLJE ZA FORMALNO VERIFIKACIJO VARNOSTNO KRITIČNIH SISTEMOVKovše, Tim (Avtor) Brezočnik, Zmago (Mentor) formalna verifikacijavarnostno kritični sistemiSpinplatforma bogatega odjemalcaV zadnjih desetletjih je področje informacijskih in komunikacijskih tehnologij doživelo izjemno pozornost tako na področju razvoja kot tudi na področju njihove rabe. Kompleksnost razvoja se je povečala, naprave, od katerih so pogosto odvisna človeška življenja, pa so postale vseprisotne. Nepravilnosti pri delovanju takšnih naprav imajo lahko za posledico negativne vplive na varnost, zato takšne sisteme imenujemo varnostno kritični sistemi. Za njihovo testiranje se namenja vedno več virov, tako časa kot denarja, pri čemer je vedno pogostejša uporaba formalnih metod. Med njimi je tudi metoda preverjanja modelov, ki jo uporablja orodje Spin. Trenutna okolja, ki za svoje delovanje uporabljajo Spin, ne omogočajo enostavnega dela z obsežnimi industrijskimi primeri, zato smo se v okviru magistrskega dela odločili razviti okolje za formalno verifikacijo varnostno kritičnih sistemov. Okolje s svojimi lastnostmi inženirju olajša celoten cikel razvoja sistema od tvorbe, verifikacije, pa do simulacije modela. Pri tvorbi modela v urejevalniku omogoča krčenje programske kode, barvanje sintakse in svetovanje rezerviranih besed. Pri verifikaciji modela je na nastavitvenih straneh mogoče enostavno izbrati varnostne in živostne lastnosti ter druge nastavitve, kot je omejitev pomnilnika, ki ga ima na voljo verifikator. Sled izvajanja, ki nastane, ko je v modelu odkrito kršenje specifikacije zahtev, je lahko zelo obsežna, zato smo v okolje vgradili pregledovalnik diagramov MSC. Ta omogoča abstrakcijo sledi, zato so diagrami preglednejši, tako da lahko razvijalec pri razhroščevanju lažje in hitreje odkrije napako v izvajanju. Razvito okolje je odprtokodno. [T. Kovše]20112011-09-01 10:20:47Magistrsko delo19864sl