December 2014 - tr-announce - lists.rwth-aachen.de

2014-15: Synthesis of State Space Generators for Model Checking Microcontroller Code
by Thomas Ströder 08 Dec '14

08 Dec '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Synthesis of State Space Generators for Model Checking Microcontroller Code Dominique Gückel AIB 2014-15 Creating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and static analysis. Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures. It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way. The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software. In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely. A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.

1 0

2014-14: HotBox: Testing Temperature Effects in Sensor Networks
by Thomas Ströder 04 Dec '14

04 Dec '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: HotBox: Testing Temperature Effects in Sensor Networks Florian Schmidt, Matteo Ceriotti, Niklas Hauser, and Klaus Wehrle AIB 2014-14 Low-power wireless networks, especially in outside deployments, are exposed to a wide range of temperatures. The detrimental effect of high temperatures on communication quality is well known. To investigate these influences under controlled conditions, we present HotBox, a solution with the following properties: (1) It allows exposition of sensor motes to a wide range of temperatures with a high degree of accuracy. (2) It supports specifying exact spatial orientation of motes which, if not ensured, interferes with repeatable experiment setups. (3) It is reasonably easy to assemble by following the information (code, PCB schematics, hardware list and crafting instructions) available online, facilitating further use of the platforms by other researchers. After presenting HotBox, we will show its performance and prove its feasibility as evaluation platform by conducting several experiments. These experiments additionally provide further insight into the influence of temperature effects on communication performance in low-power wireless networks.

1 0

2014-16: Verifying Probabilistic Systems: New Algorithms and Complexity Results
by Thomas Ströder 04 Dec '14

04 Dec '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Verifying Probabilistic Systems: New Algorithms and Complexity Results Hongfei Fu AIB 2014-16 The content of the dissertation falls in the area of formal verification of probabilistic systems. It comprises four parts listed below: 1. the decision problem of (probabilistic) simulation preorder between probabilistic pushdown automata (pPDAs) and finite probabilistic automata (fPAs); 2. the decision problem of a bisimilarity metric on finite probabilistic automata (fPAs); 3. the approximation problem of acceptance probability of deterministic-timed-automata (DTA) objectives on continuous-time Markov chains (CTMCs); 4. the approximation problem of cost-bounded reachability probability on continuous-time Markov decision processes (CTMDPs). The first two parts are concerned with equivalence checking on probabilistic automata, where probabilistic automata (PAs) are an analogue of discrete-time Markov decision processes that involves both non-determinism and discrete-time stochastic transitions. The last two parts are concerned with numerical algorithms on Markov jump processes. In Part 1 and Part 2, we mainly focus on complexity issues; as for Part 3 and Part 4, we mainly focus on numerical approximation algorithms.

1 0