liu.seSök publikationer i DiVA
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Framework For Interacting With Parameterized and Infinite State Verification Tools
Linköpings universitet, Institutionen för datavetenskap. Linköpings universitet, Tekniska högskolan.
2013 (Engelska)Självständigt arbete på avancerad nivå (magisterexamen), 20 poäng / 30 hpStudentuppsats (Examensarbete)
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.

Ort, förlag, år, upplaga, sidor
2013. , s. 38
Nationell ämneskategori
Teknik och teknologier
Identifikatorer
URN: urn:nbn:se:liu:diva-94563ISRN: LIU-IDA/LITH-EX-A--13/030—SEOAI: oai:DiVA.org:liu-94563DiVA, id: diva2:633131
Ämne / kurs
Master's programme in Computer Science
Presentation
2013-05-22, Alan Turing, Linköpings universitet, Linköping, 11:37 (Engelska)
Handledare
Examinatorer
Tillgänglig från: 2013-07-03 Skapad: 2013-06-26 Senast uppdaterad: 2013-07-03Bibliografiskt granskad

Open Access i DiVA

Thesis Report Rizwan_final - ep(2755 kB)449 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 2755 kBChecksumma SHA-512
bebce2433fe1b3f0b90af0cdcb1aa0989a4ee34ff73f4f8425aef975b86cb6192cd2b2d8d2eb6a311d08841440fca70dc3d7ecedaed7c8367b906a48835ee78d
Typ fulltextMimetyp application/pdf

Sök vidare i DiVA

Av författaren/redaktören
Abbasi, Rizwan
Av organisationen
Institutionen för datavetenskapTekniska högskolan
Teknik och teknologier

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 449 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 1535 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf