Change search
ReferencesLink to record
Permanent link

Direct link
State Space Representation for Verification of Open Systems
KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.ORCID iD: 0000-0002-0074-8786
2006 (English)In: Algebraic Methodology And Software Technology, Proceedings / [ed] Johnson, M; Vene, V, Berlin: Springer , 2006, 5-20 p.Conference paper (Refereed)
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.

Place, publisher, year, edition, pages
Berlin: Springer , 2006. 5-20 p.
, Lecture notes in computer science, ISSN 0302-9743 ; 4019
National Category
Computer Science
URN: urn:nbn:se:kth:diva-13464ISI: 000239425400004ScopusID: 2-s2.0-33746062063ISBN: 3-540-35633-9OAI: diva2:325424
11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006;Kuressaare;5 July 2006through8 July 2006
QC 20100618Available from: 2010-06-18 Created: 2010-06-18 Last updated: 2012-03-19Bibliographically approved

Open Access in DiVA

No full text


Search in DiVA

By author/editor
Aktug, IremGurov, Dilian
By organisation
Numerical Analysis and Computer Science, NADA
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
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: 43 hits
ReferencesLink to record
Permanent link

Direct link