2009

 nach oben zur Jahresübersicht

• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakow, Ralf Wimmer, Bernd Becker
  Compositional Dependability Evaluation for Statemate
  2009 IEEE Trans. on Software Engineering, Band: 35, Nummer: 2, Seiten: 274 - 292
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Software and system dependability is getting ever more important inembedded system design. Current industrial practice of model-basedanalysis is supported by state-transition diagrammatic notationssuch as Statecharts. State-of-the-art modelling tools like\textsc{Statemate} support safety and failure-effect analysis atdesign time, but restricted to qualitative properties. This paperreports on a (plug-in) extension of \textsc{Statemate} enabling theevaluation of quantitative dependability properties at design time.The extension is compositional in the way the model is augmentedwith probabilistic timing information. This fact is exploited in theconstruction of the underlying mathematical model, a uniformcontinuous-time Markov decision process, on which we are able tocheck requirements of the form: \emph{``The probability to hit asafety-critical system configuration within a mission time of 3hours is at most 0.01.''} We give a detailed explanation of theconstruction and evaluation steps making this possible, and reporton a nontrivial case study of a high-speed train signalling systemwhere the tool has been applied successfully.

2008

 nach oben zur Jahresübersicht

• Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd Becker
  Probabilistic Model Checking and Reliability of Results
  2008 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Science Press, Seiten: 207 - 212
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations of the model checking algorithms due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.\par We motivate our investigations with an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. We then analyze, at which points inaccuracies are introduced during the model checking process. We discuss first ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential correctness problems: (1) usage of exact (rational) arithmetic, (2) usage of interval arithmetic to obtain safe approximations of the actual probabilities, (3) provision of certificates which testify that the result is correct, and (4) integration of a ``degree of belief'' for each sub-formula into existing model checking tools.
• Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf Wimmer
  Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  2008 IEEE Int'l Conf. on Computer Design, IEEE Computer Society Press, Seiten: 52 - 59
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w.\,r.\,t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210\% and a speed-up of the CPU runtime up to 390\% compared to the relation-oriented approach are achieved. But there are also relevant examples, e.\,g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300\% in terms of CPU-time, showing that both approaches are efficient for different scenarios.
• Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd Becker
  The Demand for Reliability in Probabilistic Verification
  2008 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 99 - 108
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  For formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.\par First we present an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. This motivates the investigation at which points inaccuracies are introduced during the model checking process. We then give ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential problems: (1) to introduce a ``degree of belief'' for each sub-formula, (2) to use exact (rational) arithmetic, (3) to use interval arithmetic to obtain safe approximations of the actual probabilities, and (4) to provide certificates which testify that the result is correct.

2007

 nach oben zur Jahresübersicht

• Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian Herde
  On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata
  2007 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Society, Seiten: 391 - 396
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  rithmic structure of the combined SAT-LP-solver, and (2) efficiency issues in form of a counter-based design that adapts the popular concept of the VSIDS heuristics of Chaff. An empirical analysis ofour framework shows (1) the importance of guard variables related to real-valued constraints and (2) reveals an ambiguity between the number of calls of the LP-solver and the time used by the LP-solver. As a result, we propose a simple, but efficient, variable selection heuristics that takes our observations into account and experimentally overcomes the limitations of existing ones.
• Marc Herbstritt, Vanessa Struve, Bernd Becker
  Application of Lifting in Partial Design Analysis
  2007 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Seiten: 33 - 38
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the past, we have investigated satisfiability-based combinational equivalence checking and bounded model checking of partial circuit designs, i.e., circuit designs where one or more components of the design are not implemented yet. Especially for satisfiability-based bounded model checking, typically a counterexampleis generated in case that the specification property is violated. Minimizing the number of assigned variables in the satisfying assignment that corresponds to such a counterexample is the objective of lifting.In this work we show that lifting is also feasible and profitable for counterexamples obtained via satisfiability-based bounded model checking of partial designs. We provide first experimental results on this issue that show its feasibility.Furthermore, we present a novel application scenario for lifting in the context of automated blackbox synthesis. This is a useful concept that can be applied during combinational equivalence checking of partial circuit designs, where realizability of the missing componentswas already proven, but the functionality of the missing components is still unknown. As a summary, this work provides first experimental results as well as a novel concept regarding the application of lifting for the analysis of partial designs.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker
  Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation
  2007 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 203 - 212
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we present optimizations for a BDD-based algorithm for the computation of several types of bisimulations which play an important role for minimisation of large systems thus enabling their verification. The basic principle of the algorithm is partition refinement. Our proposed optimizations take this refinement-structure as well as the usage of BDDs for the representation of the system into account: (1) \emph{block forwarding} updates in-situ newly refined blocks of the partition, (2) \emph{split-driven refinement} approximates the blocks that may be refined, and (3) \emph{block ordering} heuristically suggests a good order in which the blocks will be refined.\par We provide substantial experimental results on examples from different applications and compare them to alternative approaches. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.
• Marc Herbstritt, Bernd Becker
  On Combining 01X-Logic and QBF
  2007 Int'l Conf. on Computer Aided Systems Theory, Springer Verlag, Seiten: 531 - 538
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We discuss how to combine 01X-logic and quantified booleanformulas (QBF) within a homogeneous SAT/QBF-framework in the context of bounded model checking of blackbox designs. The proposed combination allows a flexible handling of blackboxes w.r.t. computational resources. Preliminary results show the scalability of the approach.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker
  Optimization Techniques for BDD-based Bisimulation Minimization
  2007 Great Lakes Symp. on VLSI, ACM Press, Seiten: 405 - 410
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of the problem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.
• Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd Becker
  Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic
  AVACS Technical Report, Nummer: 30, 2007
• Ralf Wimmer, Holger Hermanns, Marc Herbstritt, Bernd Becker
  Towards Symbolic Stochastic Aggregation
  AVACS Technical Report, Nummer: 16, 2007

2006

 nach oben zur Jahresübersicht

• Ralf Wimmer, Tobias Nopper, Marc Herbstritt, Christoph Löffler, Bernd Becker
  Collaborative Exercise Management
  2006 World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education, Association for the Advancement of Computing in Education (AACE), Seiten: 3127 - 3134
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this work, we report on a novel tool for managing exercises used in a collaborative course organization environment at university. Our approach focuses on the separation of the content of the exercises and its layout. The latter is based on the typesetting system LaTeX. Content management of the exercises is established by a web-based interface. As a whole, our tool provides a time-saving and unambiguous workflow for collaborative, time- and place-independent exercise organization.
• Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
  Memory-aware Bounded Model Checking for Linear Hybrid Systems
  2006 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer IIS/EAS, Seiten: 153 - 162
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded Model Checking (BMC) is a successful method for refuting properties of erroneous systems. Initially applied to discrete systems only, BMC could be extended to more complex domains like linear hybrid automata. The increasing complexity coming along with these complex models, but alsorecent optimizations of SAT-based BMC, like excessive conflict learning, reveal a memory explosion problem especially for deep counterexamples. In this paper we introduce parametric data types for the internal solverstructure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver.
• Marc Herbstritt, Bernd Becker, Christoph Scholl
  Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
  2006 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Seiten: 37 - 44
• Marc Herbstritt, Ralf Wimmer, Thomas Peikenkamp, Eckard Böde, Michael Adelaide, Sven Johr, Holger Hermanns, Bernd Becker
  Analysis of Large Safety-Critical Systems: A quantitative Approach
  AVACS Technical Report, Band: 8, 2006
• Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
  Bounded Model Checking with Parametric Data Structures
  2006 BMC, Band: 174, Nummer: 3, Seiten: 3 - 16
• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker
  Compositional Performability Evaluation for STATEMATE
  2006 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Society, Seiten: 167 - 178
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  le timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from Statemate models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible. The entire tool flow has been implemented, and it is applied to a nontrivial example.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker
  Minimization of Large State Spaces using Symbolic Branching Bisimulation
  2006 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Society Press, Seiten: 9 - 14
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bisimulations in general are a powerful concept to minimize large finite state systems regarding some well-defined observational behavior. In contrast to strong bisimulation, for branching bisimulation there are only tools available that work on an explicit state space representation. In this work we present for the first time a symbolic approach for branching bisimulation that uses BDDs as basic data structure and that is based on the concept of signature refinement. First experimental results for problem instances derived from process algebraic system descriptions show the feasibility and the robustness of our approach.
• Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker
  Sigref - A Symbolic Bisimulation Tool Box
  2006 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 4218, Seiten: 477 - 492
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation. We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

2005

 nach oben zur Jahresübersicht

• Marc Herbstritt, Bernd Becker
  On SAT-based Bounded Invariant Checking of Blackbox Designs
  2005 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Seiten: 23 - 28
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Design verification by property checking is a mandatory taskduring circuit design. In this context, Bounded Model Checking (BMC) has become popular for falsifying erroneous designs. Additionally, the analysis of partial designs, i.e., circuits that are not fully specified, has recently gained attraction. In this work we analyze how BMC can be applied to such partial designs. Our experiments show that even with the most simple modelling scheme, namely 01X-simulation, a relevant number of errors can be detected. Additionally, we propose a SAT-solver that directly can handle 01X-logic.

2004

 nach oben zur Jahresübersicht

• Marc Herbstritt, Thomas Kmieciak, Bernd Becker
  On the Impact of Structural Circuit Partitioning on SAT-based Combinational Circuit Verification
  2004 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Seiten: 50 - 55
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this work we present an approach for SAT-based combinational circuit verification using partitionings of the set of primary outputs. We formally analyze the applied partitioning heuristics for the first time and present a closed verification framework incorporating traditional techniques. We report on experiments using our partitioning-based verification procedure that result in speedups of 276% on the average compared to traditional techniques.
• Marc Herbstritt, Thomas Kmieciak, Bernd Becker
  Circuit Partitioning for SAT-based Combinational Circuit Verification -- A Case Study
  , Nummer: 206, 2004
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Hardware verification is nowadays one of the most time-consuming tasks during chip design. In the last few years SAT-based methods have become a core technology in hardware design, especially for the verification of combinational parts of the circuits. Verifying the equivalence of some specification and a corresponding implementation is typically done by building a so-called miter. In practice this miter is often build for each pair of primary outputs or for all primary outputs at once. In this work we have a closer look on partitioning the primary outpouts of the circuit and how structural partitionings can speed-up the verification process when SAT-based methods are used.
• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf Wimmer
  Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
  2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 65 - 75
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of different verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.

2003

 nach oben zur Jahresübersicht

• Marc Herbstritt, Bernd Becker
  Conflict-based Selection of Branching Rules
  2003 Int'l Conf. on Theory and Applications of Satisfiability Testing, Springer, Band: 2919, Seiten: 441 - 451
• Marc Herbstritt, Bernd Becker
  Conflict-based Selection of Branching Rules in SAT-Algorithms
  2003 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 189 - 198

2001

 nach oben zur Jahresübersicht

• Marc Herbstritt
  zChaff: Modifications and Extensions
  , Nummer: 188, 2001
• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Don't Care Minimization of *BMDs: Complexity and Algorithms
  2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 45 - 57
• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Exploiting Don't Cares to Minimize *BMDs
  2001 IEEE Int'l Symp. on Circuits and Systems, Band: 5, Seiten: 191 - 194

2000

 nach oben zur Jahresübersicht

• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Exploiting Don't Cares to Minimize *BMDs
  , Nummer: 141, 2000
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present for the first time methods to minimize *BMDs exploiting don't care conditions. These minimization methods can be used during the verification of circuits by *BMDs. By changing function values for input vectors, which are in the don't care set, smaller *BMDs can be computed to keep peak memory consumption during *BMD construction as low as possible. We determine the complexity of the problem of don't care minimization for *BMDs and thus justify the use of heuristics to approximate the solution. Preliminary experimental results prove our heuristcs to be very effective in minimizing *BMD sizes.

1999

 nach oben zur Jahresübersicht

• Rolf Drechsler, Marc Herbstritt, Bernd Becker
  Grouping Heuristics for Word-level Decision Diagrams
  1999 IEEE Int'l Symp. on Circuits and Systems, Seiten: 411 - 415
• Rolf Drechsler, Marc Herbstritt, Bernd Becker
  Grouping Heuristics for Word-level Decision Diagrams
  1999 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 41 - 50