Show simple item record

dc.contributor.author
Lampka, Kai
dc.date.accessioned
2022-08-10T08:02:43Z
dc.date.available
2017-06-09T00:14:40Z
dc.date.available
2022-08-10T08:02:43Z
dc.date.issued
2009-08
dc.identifier.uri
http://hdl.handle.net/20.500.11850/21568
dc.description.abstract
This paper introduces a new technique for generating Binary Decision Diagrams (BDDs) representing high-level model’s underlying state/tran- sition systems. The obtained decision diagram may serve as input for various analysis methods such as symbolic (probabilistic) model checking and/or Markovian performance and reliability analysis. As usual the pro- posed technique makes use of partitioned symbolic reachability analysis. However, contrary to existing techniques it neither relies on pregenerated symbolic representations of transition relations, nor does it make use ofstandard BDD-manipulating algorithms. Instead, symbolic reachability analysis is carried out by means of customized BDD-algorithms directly synthesized from high-level models to be analyzed. Overall the presentedapproach yields the core of a new tool bench for the symbolic analysis of state-based system descriptions. The tool bench is implemented on topof the Eclipse Modeling Framework and exploits Java Emitter Templates for code synthesis. Standard benchmark models show that for generating high-level models underlying state/transition systems significant improve- ments with respect to CPU time and memory consumption can be real- ized, ultimately allowing the verification of larger and much more complex systems.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH Zurich, Computer Engineering and Networks Laboratory
en_US
dc.title
Symbolic Reachability Graph Generation for High-level Models based on Synthesized Operators
en_US
dc.type
Report
ethz.journal.title
TIK Report
ethz.journal.volume
307
en_US
ethz.size
18 p.
en_US
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.date.deposited
2017-06-09T00:15:04Z
ethz.source
ECIT
ethz.identifier.importid
imp59364ccd828b232030
ethz.ecitpid
pub:34234
ethz.eth
yes
en_US
ethz.availability
Metadata only
en_US
ethz.rosetta.installDate
2017-07-19T01:25:19Z
ethz.rosetta.lastUpdated
2017-07-19T01:25:19Z
ethz.rosetta.exportRequired
true
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Symbolic%20Reachability%20Graph%20Generation%20for%20High-level%20Models%20based%20on%20Synthesized%20Operators&rft.jtitle=TIK%20Report&rft.date=2009-08&rft.volume=307&rft.au=Lampka,%20Kai&rft.genre=report&
 Search print copy at ETH Library

Files in this item

FilesSizeFormatOpen in viewer

There are no files associated with this item.

Publication type

Show simple item record