| Requirements Specification |
The requirements concerning the control
part of the system under development (SUD for short) are described by
languages with formal semantics such as Message Sequence Charts (MSC),
higher order logic and various dialects of Temporal Logics (TL). These
languages allow for the specification of discrete as well as continuous
aspects of the SUD including hard real-time
requirements. The data transformation part of the SUD is described in
object-oriented style by means of type constraints. |
|---|
|
| Specifications |
For the abstract modeling of systems, executable
specification formalisms are used which allow for animation, validation,
and verification of specifications. This includes UML (Universal Modeling
Language), SDL (System Description Language), automata-based formalisms,
object-oriented languages and synchronous languages. |
|---|
|
| Verification |
Algorithmic techniques (enumerative and symbolic
model-checking) and deductive techniques are employed in order to
prove in a mathematically rigorous way that the specified systems have
certain desired properties such as absence of deadlock and live-lock,
determinism, as well as system specific properties formulated in the
requirements specification languages. |
|---|
|
| Compositionality |
Compositional verification techniques reduce the
verification of large programs to the independent verification of their
parts without imposing any need about additional knowledge about the
implementation of their parts. Compositional verification represent one
of the hopeful direction for the verification of really large programs.
|
|---|
|
| Test-Automation |
Methods for automated test generation, -execution,
and -evaluation based on the CSP formalism (Communicating Sequential
Processes) are investigated as well as automated test-evaluation against Z
specification. |
|---|
| Statemate |
Development, validation and documentation of control
systems based on synchronous, graphical formalisms, rapid prototyping and
automatic code generation, iLogix (co) |
|---|
|
| Rhapsody |
Development of transformational and embedded systems
based on UML, object-orientation and automatic code generation, iLogix (co). |
|---|
|
| SMV |
A symbolic model-checker, Carnegie Mellon University
(co). |
|---|
|
| Spin |
An enumerative model-checker, Lucent Technology/Bell Labs
(ac). |
|---|
|
| KRONOS |
A model-checker for timed automata, Verimag
(ac). |
|---|
|
| HyTech |
A model-checker for linear hybrid systems, Berkley
(ac). |
|---|
|
| PVS |
An interactive theorem prover, SRI (ac). |
|---|
|
| VVT-RT |
Test-automation based on CSP, University of Bremen
(ac). |
|---|
|
| Disces |
A model-checker for Condition/Event Systems
(own). |
|---|
|
| Moces |
A model-checker for Statecharts specifications
(own). |
|---|
|
| InVeSt |
Combined model-checking and deductive techniques for
the verification of Timed Automata (own). |
|---|
|
| TVT |
A translation validation tool for Signal to C code
generators (own). |
|---|
|
| co=commercial tool, ac= academic tool,
own=own development |
|---|