20.500.12556/DKUM-19864 OKOLJE ZA FORMALNO VERIFIKACIJO VARNOSTNO KRITIČNIH SISTEMOV Environment for Formal Verification of Safety Critical Systems V 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. In recent decades, information and communications technologies have received a great deal of attention, both from the developmental as well as the applicational point of view. The level of developmental complexity has increased and the devices, on which human lives are often depending, have become ubiquitous. Irregularities in the operational functions of such devices can negatively affect the level of safety, which is why systems of such nature are referred to as safety critical systems. More and more resources, both in the form of time and money, are being invested into system testing, prevalently undertaken with formal methods. One of them is also the model checking method, which is incorporated into the Spin software tool. Current environments based on Spin are not suitable for simple operations based on complex industrial examples, which is why we have chosen to develop an environment for formal verification of safety critical systems within the framework of this master’s thesis. The properties of the environment make it easier for the engineer to complete the system development cycle; from initial design, through verification, all the way to model simulation. When designing the model in the editor, the environment in question enables code folding, syntax highlighting and reserved word assistance. During model verification, the preference pages act as platforms for selecting liveness properties and other settings, such as for example the memory limit allotted to the verificator. An execution trail, which is established when a requirement specification violation is detected in the model, can be quite extensive. With regard to this fact, we have equipped the environment with an MSC diagram viewer. This tool enables trail abstraction, what renders the diagrams clearer and consequently makes it easier for the developer to detect an execution error quicker during the debugging process. The environment developed is an open source software. formalna verifikacija varnostno kritični sistemi Spin platforma bogatega odjemalca formal verification safety critical systems Spin Rich Client Platform true true false [T. Kovše] Slovenski jezik Angleški jezik Magistrsko delo 2011-09-01 10:20:47 2011-09-01 10:36:03 2022-04-13 15:43:06 2023-12-26 03:22:16 2011 0 Maribor 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 004.414.23:621.39(043.2) 15279126 URN:SI:UM:DK:0RQKQBZM MAG_Kovse_Tim_2011.pdf MAG_Kovse_Tim_2011.pdf 1 06A4C1585FC7E062D8755631413AC7DD 60f02520e4e9ebae84084181226701099bc34cc76b502e125bb11a7b8722c510 7b23a879-7c05-11eb-bb7a-00155d0001ca 20.500.12556/dkum/867bf1ef-2f7e-425f-a545-d11db1971ac6 https://dk.um.si/Dokument.php?lang=slv&id=24275 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0