Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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
State space representation for verification of open systems
KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
2006 (Engelska)Licentiatavhandling, monografi (Övrigt vetenskapligt)
Abstract [en]

When designing an open system, there might be no implementation available for cer- tain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. In this thesis, we present a framework for the verification of open systems through explicit state space representation.

We propose Extended Modal Transition Systems (EMTS) as a suitable structure for representing the state space of open systems when assumptions on components are writ- ten in the modal μ-calculus. EMTSs are based on the Modal Transition Systems (MTS) of Larsen. This representation supports state space exploration based verification tech- niques, and provides an alternative formalism for graphical specification. In interactive verification, it enables proof reuse and facilitates visualization for the user guiding the verification process.

We present a two-phase construction from process algebraic open system descriptions to such state space representations. The first phase deals with component assumptions, and is essentially a maximal model construction for the modal μ-calculus that makes use of a powerset construction for the fixed point cases. In the second phase, the models obtained are combined according to the structure of the open system to form the complete state space. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process creation. We suggest a tableau-based proof system for establishing open system properties of the state space representation. The proof system is sound and it is complete for modal μ-calculus formulae with only prime subformulae.

A complete framework based on the state space representation is offered for the auto- matic verification of open systems. The process begins with specifying the open system by a process algebraic term with assumptions. Then, the state space representation is ex- tracted from this description using the construction described above. Finally, open system properties can be checked on this representation using the proof system.

Ort, förlag, år, upplaga, sidor
Stockholm: Numerisk analys och datalogi , 2006. , s. viii, 100
Serie
Trita-CSC-A, ISSN 1653-5723 ; 2006:3
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:kth:diva-3973ISBN: 91-7178-341-5 (tryckt)OAI: oai:DiVA.org:kth-3973DiVA, id: diva2:10232
Presentation
2006-05-31, E3, KTH, Osquars Backe 14, Stockholm, 10:00
Opponent
Handledare
Anmärkning
QC 20101108Tillgänglig från: 2006-05-17 Skapad: 2006-05-17 Senast uppdaterad: 2018-01-14Bibliografiskt granskad

Open Access i DiVA

fulltext(732 kB)393 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 732 kBChecksumma SHA-1
ce6b845a603f25aeedbf24fe35065c0d62bee4552504e28c5061d4fda4a2cdf181dc9e82
Typ fulltextMimetyp application/pdf

Sök vidare i DiVA

Av författaren/redaktören
Aktug, Irem
Av organisationen
Numerisk Analys och Datalogi, NADA
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 393 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.

isbn
urn-nbn

Altmetricpoäng

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

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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