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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:liu:diva-94563ISRN: LIU-IDA/LITH-EX-A--13/030—SEOAI: oai:DiVA.org:liu-94563DiVA: diva2:633131
Subject / course
Master's programme in Computer Science
Presentation
2013-05-22, Alan Turing, Linköpings universitet, Linköping, 11:37 (English)
Supervisors
Examiners
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)373 downloads
File information
File name FULLTEXT01.pdfFile size 2755 kBChecksum SHA-512
bebce2433fe1b3f0b90af0cdcb1aa0989a4ee34ff73f4f8425aef975b86cb6192cd2b2d8d2eb6a311d08841440fca70dc3d7ecedaed7c8367b906a48835ee78d
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: 373 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: 1050 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf