Static byte-code analysis for state space reduction

Quirós Araya, Gustavo

doi:999910310676

Static byte-code analysis for state space reduction

Quirós Araya, Gustavo^RWTH*

2011

ImpressumAachen : Publikationsserver der RWTH Aachen University 2011

UmfangVIII, 101 S.

Aachen, Techn. Hochsch., Masterarbeit, 2006

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Hauptberichter/Gutachter

Online
URN: urn:nbn:de:hbz:82-opus-36528
DOI: 10.18154/RWTH-CONV-144790
URL: https://publications.rwth-aachen.de/record/229985/files/3652.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Programmanalyse (Genormte SW) ; Compiler (Genormte SW) ; Model Checking (Genormte SW) ; Zustandsraum (Genormte SW) ; Programmoptimierung (Genormte SW) ; Verteiltes System (Genormte SW) ; Informatik (frei) ; program analysis (frei) ; compilers (frei) ; state space reduction (frei) ; program optimisation (frei) ; distributed systems (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: I.6.4 * D.3.4 * C.2.4

Kurzfassung
NIPS is a virtual machine for the generation of state-transition systems of concurrent models, and is designed to serve as a foundation for the development of model checking applications. Like any explicit-state representation, the transition systems produced by NIPS suffer from the state-explosion problem, by which models have exponentially large state spaces. This work is dedicated to the reduction of the effect of the state-explosion problem in NIPS. State space reduction works by obtaining a reduced state-transition system from a model, which is equivalent to the original system under a given specification, or a given set of specifications. Model checking may be applied to the reduced system instead of to the original one, thus obtaining the same result in a more efficient manner. NIPS features a byte-code language for encoding concurrent models. High-level modeling languages may be compiled to this byte-code, and the interpretation of the byte-code by the machine results in the construction of the model’s state space representation. This architecture allows us to implement on-the-fly reductions merely by transforming the byte-code to another whose state-transition system is a reduced version of the original, and employing information gathered from static analysis of the byte-code in the process.

OpenAccess:
PDF