OKOLJE ZA FORMALNO VERIFIKACIJO VARNOSTNO KRITIČNIH SISTEMOV

Kovše, Tim

| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

First page > Show document

Show document

Title:	OKOLJE ZA FORMALNO VERIFIKACIJO VARNOSTNO KRITIČNIH SISTEMOV
Authors:	ID Kovše, Tim (Author) ID Brezočnik, Zmago (Mentor) More about this mentor...
Files:	MAG_Kovse_Tim_2011.pdf (4,89 MB) MD5: 06A4C1585FC7E062D8755631413AC7DD PID: 20.500.12556/dkum/867bf1ef-2f7e-425f-a545-d11db1971ac6
Language:	Slovenian
Work type:	Master's thesis
Organization:	FERI - Faculty of Electrical Engineering and Computer Science
Abstract:	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.
Keywords:	formalna verifikacija, varnostno kritični sistemi, Spin, platforma bogatega odjemalca
Place of publishing:	Maribor
Publisher:	[T. Kovše]
Year of publishing:	2011
PID:	20.500.12556/DKUM-19864
UDC:	004.414.23:621.39(043.2)
COBISS.SI-ID:	15279126
NUK URN:	URN:SI:UM:DK:0RQKQBZM
Publication date in DKUM:	01.09.2011
Views:	2829
Downloads:	173
Metadata:
Categories:	KTFMB - FERI
:	Copy citation

Average score:	(0 votes)
Your score:	Voting is allowed only for logged in users.
Share:

Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Secondary language

Language:	English
Title:	Environment for Formal Verification of Safety Critical Systems
Abstract:	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.
Keywords:	formal verification, safety critical systems, Spin, Rich Client Platform

Comments

Leave comment

You must log in to leave a comment.

Comments (0)

0 - 0 / 0

There are no comments!

Back