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

Direktlänk
Referera
Referensformat
  • apa
  • 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.
KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.ORCID-id: 0000-0002-0074-8786
2006 (Engelska)Ingår i: Algebraic Methodology And Software Technology, Proceedings / [ed] Johnson, M; Vene, V, Berlin: Springer , 2006, s. 5-20Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. When component assumptions are expressed in Hennessy-Milner logic (HML), the state space of open systems can be naturally represented with modal transition systems (NITS), a graphical specification language equiexpressive with HML. Having an explicit state space representation supports state space exploration based verification techniques, Besides, it enables proof reuse and facilitates visualization for the user guiding the verification process. in interactive verification. As an intuitive representation of system behavior, it aids debugging when proof generation fails in automatic verification.

However, HML is not expressive enough to capture temporal assumptions. For this purpose, we extend MTSs to represent the state space of open systems where component assumptions are specified in modal mu-calculus. 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 p-calculus. 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. For establishing open system properties based on the representation, we present a proof system which is sound and complete for prime formulae.

Ort, förlag, år, upplaga, sidor
Berlin: Springer , 2006. s. 5-20
Serie
Lecture notes in computer science, ISSN 0302-9743 ; 4019
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:kth:diva-13464ISI: 000239425400004Scopus ID: 2-s2.0-33746062063ISBN: 3-540-35633-9 (tryckt)OAI: oai:DiVA.org:kth-13464DiVA, id: diva2:325424
Konferens
11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006;Kuressaare;5 July 2006through8 July 2006
Anmärkning
QC 20100618Tillgänglig från: 2010-06-18 Skapad: 2010-06-18 Senast uppdaterad: 2018-01-12Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Scopus

Personposter BETA

Gurov, Dilian

Sök vidare i DiVA

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

Sök vidare utanför DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetricpoäng

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

Direktlänk
Referera
Referensformat
  • apa
  • 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