Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Test and Verification 2005
There is a strong need for the use of
advanced,
systematic techniques and tools that support the system validation
process. [
Klaus Havelund ]
Brief
course description
Software is becoming
increasingly complex and there is a growing awareness within software
engineering
practice that both formal verification techniques as well as testing
techniques
are needed in order to deal with this growing complexity. This is
in particular true in areas such as embedded systems used in consumer
electronics,
time dependent systems occurring in safety critical systems and
communication
protocols from the telecommunication industry.
The focus of this
course is on techniques and software-tools that can be used to assess
the
quality and correctness of software systems. The first part of the
course
considers tools and techniques for formal verification of system
designs.
The last part of the course considers tools and techniques for testing
system implementations.
In a (logical) first part
of the course, particular emphasis will be put on our own real-time
validation
tool UPPAAL, the commercial tools visualSTATE
and Cinderalla. In the course we will
toevaluate the usefulness
of the various features of these tools. Emphasis will be on
application
and hands-on experiment with the tools on small case-studies.
Uppaal
allows for the modeling, validation and automatic verification of
properties
of real-time systems and communication protocols The underlying
description
language and specification formalism --- timed automata and timed
temporal
logic --- will be dealt with in detail. The theoretical and
practical
aspects of the tool will be studied. To enable effective validation
of
systems special attention is given to modeling and abstraction
techniques
that help to limit the complexity of the models used.
visualSTATE is a toolset
that supports analysis, design, prototyping, validation, and
verification through simulation, code generation and testing of
systems.
The toolset is based on the UML and MSC
standards languages. visualSTATE provides graphical editors,
simulators,
a C code generator targeting real-time OS and network protocols, and a
design-level debugger.
Cinderella is a collection of software development tools supporting standardised notations like SDL, ASN.1, MSC, and UML for system design, specification and implementation.
SDL (Specification and Description Language) graphical specification language standardized by ITU (International Telecommunication
Union). Although SDL is widely used in the telecommunications field, it is not designed specifically for describing telecommunications services. Rather SDL is a general purpose specification language for communication systems and embedded systems.
In the (logical) second part
of the course, emphasis will be on methods and techniques for
testing.
In addition, the
course will involve guest lectures from industry, e.g. presentations
from IAR
Systems A/S (the provider of visualSTATE), presentations of SDL/Cinderalla by
Professor Andreas Prinz, Agder University College, Norway, and presentations on testing
in
current industrial practise.
Objectives
The aims of the
course
are that the students become familiar with the possibility of
validating
software systems based on formal models and specifications (in
particular
of real-time and embedded systems) with the aid of software tools for
the
verification and analysis, and that they learn practical techniques and
methods for testing software systems.