Department of Software Engineering - University Erlangen-Nuremberg
Tools used at the Chair of Sortware Engineering
During the requirements phase the system envisaged is modelled, e. g. by means of Petri Nets.
On the basis of this model application-specific requirements have to be analysed and validated.
The analysis concerns among others the reachability of desired system states and the proof that
unsafe states remain unreachable. Petri Nets are particularly appropriate for the description of cooperating and concurrent processes and,
thanks to the graphical representation, also support the communication between customer and developer.
Time Petri Nets
The expressiveness of ordinary Petri Nets can be augmented by introducing time by means of so-called Time Petri Nets.
This additional expressiveness is gained at the expense of decidability, but it permits to analyse real time requirements
posed to embedded systems.
- TINA (TIme petri Net Analyzer)
Similarly to Petri nets, model checkers are applied for modelling and analysing system behaviour and overall requirements.
During the analysis the fulfillment of particular requirements is either proven or falsified by providing counter examples.
The latter decisively supports fault localisation and thereby extends the functionality of most other verifiers.
Moreover, model checking can also be applied later on during the development, e. g. at code-level,
in order to prove that the also final product fulfils relevant requirements.
- NuSMV (NEW Symbolic Model Checker)
Theorem Proving is applied in order to derive the desired system properties from the formalized system requirements.
To do so, the system requirements are expressed in terms of axioms and algebraic specifications,
on the basis of which the desired system properties (formulated as theorems) may be proven using dynamic logics.
If the theorem envisaged cannot be proven this may be due to incorrect system requirements or to their incorrect formalisation.
Furthermore, Theorem Proving supports the proof of system properties at the level of (pseudo-)code by use of Hoare-Logic.
- KIV (Karlsruhe Interactive Verifier)
Object-Oriented Analysis and Design
UML is adopted as the description language for object-oriented analysis and design.
It is used to describe static and dynamic views of the system to be developed.
The diagrams formulated with the UML can be extended by means of additional constructs like OCL and AS.
Tools are used to draw the UML diagrams and to automatically generate program code skeletons from them.
- TCC (Together Control Center)
Metrics are used to determine quantitative properties of software.
They are usually determined by static analysis of the source code including information on data flow and control flow.
Many tools used for OOAD provide a set of metrics.
Software Engineering provides support in the interpretation of such parameters as complexity indicators
for the various phases of the software lifecycle.
Structural tests aim at executing a large part of the data flow resp. and control flow of source code.
For this purpose, tools supporting the generation of test cases and the check of the test results are used.
By instrumenting the source code, the coverage achieved during testing can be determined.
During development and evolution of large software systems, it is important to keep track of and
distinguish between different versions, releases and customer-specific variants. Tools support the management
of all artifacts of the software lifecycle (requirements analysis, specification, analysis and design documents,
source code, test cases and drivers, user manuals etc.) during development and maintenance.
- cvs (Concurrent Versions System)
Bug Reporting and Tracking
It is necessary to record detailed error messages or change requests of customers during maintenance of
software systems, and to subject this information to an accurately pre-defined handling process.
Tools may help by collecting incoming messages, categorizing them and assigning them to responsible software developers.
All subsequent activities involved with bug searching and bug fixing have to be recorded by the tool and
- as far as required - be reported back to the initial submitter of bug reports
- gnats (A Tracking System)