liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
A Framework For Interacting With Parameterized and Infinite State Verification Tools
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2013 (English)Independent thesis Advanced level (degree of Master (One Year)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

We develop a tool to explore the behavior of parameterized systems (i.e., systems consisting of an arbitrary number of identical processes that synchronize using shared variables or global communications) and to ease user interaction with tools that verify them. The tool includes a user friendly GUI that allows the user to describe a parameterized system and to perform guided, interactive or random simulation. This tool empowers the user to plug in several independent verifiers to perform verification. A mockup verifier is developed in order to facilitate the development of the tool and testing the required functionalities. The mockup verifier involves parsing descriptions of the parameterized systems to be analyzed. In order to interact with the verifier, the tool is user friendly and flexible in the sense that the user can plug in a verifier developed in any language as long as it allows to perform a number of basic computations on the parameterized system (such as the set of enabled transitions or the set of successor configurations). In order to plug in a new tool, our tool needs to be able to make use of these operations, for instance using a wrapper written for a verifier particular to a class of parameterized systems. Given these operations, our tool enables the user to carry out various types of simulations like random, interactive or guided simulations. Moreover, our tool can submit verification queries to the underlying verifier and walk the user through the generated counter examples as if it was a simulation session.

Place, publisher, year, edition, pages
2013. , 38 p.
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-94563ISRN: LIU-IDA/LITH-EX-A--13/030—SEOAI: diva2:633131
Subject / course
Master's programme in Computer Science
2013-05-22, Alan Turing, Linköpings universitet, Linköping, 11:37 (English)
Available from: 2013-07-03 Created: 2013-06-26 Last updated: 2013-07-03Bibliographically approved

Open Access in DiVA

Thesis Report Rizwan_final - ep(2755 kB)317 downloads
File information
File name FULLTEXT01.pdfFile size 2755 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Abbasi, Rizwan
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 317 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 742 hits
ReferencesLink to record
Permanent link

Direct link