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.
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.