tr-announce

Download

tr-announce@lists.rwth-aachen.de

June 2007

1 participants
2 discussions

2007-08: Achieving Highly Reliable Embedded Software: An empirical evaluation of different approaches
by Peter Schneider-Kamp 05 Jun '07

05 Jun '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: Achieving Highly Reliable Embedded Software: An empirical evaluation of different approaches Falk Salewski and Stefan Kowalewski AIB 2007-08 Designing highly reliable embedded software is a challenge and several approaches are known to improve the reliability of this software. However, all approaches have their advantages and disadvantages which makes empirical evaluations investigating their potentials necessary. In this paper, different approaches of software reliability improvement for embedded systems were compared on basis of experiments conducted at our institute. The first approach is an instance of N-version programming based on forced diversity. Two fundamentally diverse hardware platforms (microcontroller and CPLD/FPGA) were used to force diversity. Another experiment was conducted in which participants designed their software on one hardware platform only. The second half of this experiment was used for review and testing. Based on our experiments, the potentials of our application of N-version programming, review and testing are compared with respect to different fault categories (specification, implementation, application) identified during evaluation.

1 0

2007-09: A Probabilistic Justification of the Combining Calculus under the Uniform Scheduler Assumption
by Peter Schneider-Kamp 04 Jun '07

04 Jun '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Probabilistic Justification of the Combining Calculus under the Uniform Scheduler Assumption Tina Kraußer, Heiko Mantel, and Henning Sudbrock AIB 2007-09 The combining calculus provides a framework for analyzing the information flow of multi-threaded programs. The calculus incorporates so called plug-in rules for integrating several previously existing analysis techniques. By applying a plug-in rule to a subprogram, one decides to analyze this subprogram with the given analysis technique, and not with the rules of the combining calculus. The novelty of the combining calculus was that one can analyze the information flow security of a given program by using multiple analysis techniques in combination. It was demonstrated that this flexibility leads to a more precise analysis, allowing one to successfully verify the security of some programs that cannot be verified with any of the existing analysis techniques in isolation. In MSK07, the soundness of the combining calculus is proved for a possibilistic characterization of information flow security. This characterization assumes a purely nondeterministic scheduling of concurrent threads. In this report, we demonstrate that the combining calculus is also sound for a probabilistic characterization of security that assumes a uniform scheduler. This result further increases the confidence in the combining calculus as a reliable and flexible tool for formally analyzing the information flow security of multi-threaded programs.

1 0