Show simple item record

dc.contributor.authorLilleskare, Andreas
dc.date.accessioned2017-08-10T09:17:06Z
dc.date.available2017-08-10T09:17:06Z
dc.date.issued2017-06-21
dc.date.submitted2017-06-20T22:00:08Z
dc.identifier.urihttps://hdl.handle.net/1956/16257
dc.description.abstractExplicit-state model checking is a formal software verification technique that differs from peer review and unit testing, in that model checking does an exhaustive state space search. With model checking one takes a system model, traverse all reachable states, and check theses according to formal stated properties over the variables in the model. The properties can be expressed with linear temporal logic or computation tree logic, and can for example be that the value of some variable x should always be positive. When conducting an explicit state space exploration one is guaranteed that the complete state space is checked according to the given property. This is not the case in for instance unit testing, where only fragments of a system are tested. In the case that a property is violated, the model checking algorithm should present an error trace. The error trace represents an execution path of the model, demonstrating why it does not satisfy the property. The main disadvantage of model checking, is that the number of reachable states may grow exponentially in the number of variables. This is known as the state explosion problem. This thesis focuses on explicit-state model checking using the sweep-line method. To combat the state explosion problem, the sweep-line method exploits the notion of progress that a system makes, and is able to delete states from memory on-the-fly during the verification process. The notion of progress is captured by progress measures. Since the standard model checking algorithms rely upon having the whole state space in memory, they are not directly compatible with the sweep-line method. We survey differences of standard model checking algorithms and the sweep-line method, and present previous research on verifying properties and providing error traces with the sweep-line method. The new contributions of this thesis are as follows: (1) We develop a new general technique for providing an error trace for linear temporal logic properties, verified using the sweep-line method; (2) A new algorithm for verifying two key computation tree logic properties, on models limited to monotonic progress measures; (3) A unified library for the sweep-line method is implemented with the algorithms developed in this thesis, and the previous developed algorithms for verifying safety properties and linear temporal logic property checking. All algorithms implemented, are validated by checking properties on a model of a stop-and-wait communication protocol.en_US
dc.language.isoengeng
dc.publisherThe University of Bergenen_US
dc.titleModel Checking with the Sweep-Line Methoden_US
dc.typeMaster thesis
dc.date.updated2017-06-20T22:00:08Z
dc.rights.holderCopyright the Author. All rights reserveden_US
dc.description.degreeMasteroppgave i informatikken_US
dc.description.localcodeINF399
dc.subject.nus754199eng
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400::Informasjons- og kommunikasjonsvitenskap: 420en_US
fs.subjectcodeINF399
fs.unitcode12-12-00


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record