|
Competence Center Verification & Testing - Projects
 Runtime Reflection
is a project for establishing methods to dynamically analyse
reactive distributed systems at runtime. The approach
is layered and modular in that we provide the means for first
detecting failures of a system by means of runtime verification and
secondly, provide means for identifying their causes by means
of a detailed diagnosis. As such, diagnoses can be
subsequently used in order to trigger recovery measures, or to
store detailed log-files for off-line analysis.
Check out the Runtime
Reflection homepage for further details, examples,
downlaods etc.
SALT is a temporal
specification language that is similar in spirit to programming
languages like C and Java and is therefore well suited for
software engineers. Its expressiveness, on the other side,
covers LTL, or, when the realtime operators of SALT are used,
covers TLTL (Timed LTL).
Parts of SALT are similar in spirit to the specification language
Sugar/PSL, a domain specific language used in hardware
industry. SALT, however, is designed mainly for software
systems. SALT is heavily influenced by the SpecPatterns
approach, which collects and documents typical patterns
occurring in industrial specifications to make them available to
non-expert users. Contrary, however, SALT aims at supporting
typical patterns by operators of its language.
Check out SALT's homepage
for further details, examples, downlaods etc.
AutoHMI is a project about the model-based design,
specification, and verification of automotive human-machine
interfaces (HMIs). In particular, we propose an approach for
modeling the behavior, structure, and properties of HMIs, and
to facilitate their automatic verification by means of model
checking. We guide this process by using a well-defined
quality model that applies to automotive HMIs and gives firm
criteria not only to establish correctness, but also to reason
about their usability and, ultimately, user acceptance.
Within
INI.TUM (Ingolstadt Institutes of
TU München), methods for the application of
model-based testing in the automotive industry are
developed. Especially in this domain, the expenses for
defining test cases manually increases enormously. At the same
time, the continously increasing complexity of software
intensive functions in cars bears higher risks of undetected
errors. In the project adequate modeling techniques are
proposed for formally specifying the requirements which may
additionally be used for test case generation. The test cases
shall be generated in a way that the combination of
requirements and known critical design decisions are
considered.
INI.TUM is a cooperation between TUM and Audi AG. Check
out the projects' Homepage at INI.TUM (in german
or english).
AutoFocus 2 Test Case
Generator extends the CASE tool AutoFocus 2 by
functionality for test case generation. Here we use
Constraint Logic Programming (CLP) for test case
generation. An AutoFocus model is translated into an
equivalent CLP program. Then test case generation is done by
solving goals in CLP which define the test case specification.
|
