Category: 2012

Runtime Verification of Microcontroller Binary Code

Runtime verification bridges the gap between formal verification and testing by providing techniques and tools that connect executions of a software to its specification without trying to prove the absence of errors. This article presents a framework for runtime verification

Efficient and Trustworthy Tool Qualification for Model-Based Testing Tools

The application of test automation tools in a safety-critical context requires so-called tool qualification according to the applicable standards. The objective of this qualification is to justify that verification steps automated by the tool will not lead to faulty systems

Real-Time Runtime Verification on Chip

We present an algorithmic framework that allows on-line monitoring of past-time MTL specifications in a discrete time setting. The algorithms allow to be synthesized into efficient observer hardware blocks, which take advantage of the highly-parallel nature of hardware designs. For

ArcadePLC: A Verification Platform for Programmable Logic Controllers

This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the underlying

Access-Based Localization for Octagons

Access-based localization is a two-step process. First, the set of abstract memory locations that are accessed in a procedure are determined. Then, in a subsequent fixed point iteration, the input to the respective procedure is reduced to those variables that

Abstract Interpretation of Microcontroller Code: Intervals Meet Congruences

Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs. In particular, since registers are often memory mapped, it is necessary to show that an indirect store operation does not accidently mutate a register. To

Benchmark Analysis of GTL-Backends using Client-Server Mutex

This white-paper reports on benchmark measurements performed for the alternative model-checking backends of the contract specification language GTL. The GTL has been developed in context of the VerSyKo project. The considered backends are the model-checking tools SPIN and UPPAAL. The

Loop Leaping with Closures

Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop

Transfer Function Synthesis without Quantifier Elimination

Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs by operating over propositional Boolean formulae. The drawback of this method is that it relies on existential quantifier elimination, which induces a computational bottleneck. The