liu.seSearch for publications in DiVA
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet 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 (engelsk)Independent thesis Advanced level (degree of Master (One Year)), 20 poäng / 30 hpOppgave
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.

sted, utgiver, år, opplag, sider
2013. , s. 38
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-94563ISRN: LIU-IDA/LITH-EX-A--13/030—SEOAI: oai:DiVA.org:liu-94563DiVA, id: diva2:633131
Fag / kurs
Master's programme in Computer Science
Presentation
2013-05-22, Alan Turing, Linköpings universitet, Linköping, 11:37 (engelsk)
Veileder
Examiner
Tilgjengelig fra: 2013-07-03 Laget: 2013-06-26 Sist oppdatert: 2013-07-03bibliografisk kontrollert

Open Access i DiVA

Thesis Report Rizwan_final - ep(2755 kB)460 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 2755 kBChecksum SHA-512
bebce2433fe1b3f0b90af0cdcb1aa0989a4ee34ff73f4f8425aef975b86cb6192cd2b2d8d2eb6a311d08841440fca70dc3d7ecedaed7c8367b906a48835ee78d
Type fulltextMimetype application/pdf

Søk i DiVA

Av forfatter/redaktør
Abbasi, Rizwan
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 460 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

urn-nbn

Altmetric

urn-nbn
Totalt: 1700 treff
RefereraExporteraLink to record
Permanent link

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