Software written for telecommunication applications has to meet
high quality demands. A telephone switch, for example, should be very
robust, which is expressed in a "downtime" of at most a few minutes
a
year.
Special techniques and procedures in the design and development of
the
software guarantee most of its quality. In addition many effort is
put
in testing the software and hardware when development has finished.
Software verification seems a promissing candidate for reducing the
costs of testing by finding bugs in an early stage and for improving
the
robustness by finding bugs that would not have been caught by testing.
In cooperation with the Swedish institute of computer science, Ericsson
Telecom has started to investigate where and how verification techniques
can be used and what results are to be expected.
For this reason, a verification tool is under development. In order
to
make the tool as effective as possible, we run case-studies during
it's
development. By considering parts of real telecom software, we hope
to
be able to find solutions for and to keep our focus on the real
problems.
The software part of a typical telecommunication project may consists
of
near half a million lines of code. The software is highly concurrent,
running hundreds of thausands of processes on several processors. The
code for the processes itself is well understandable, but the
interaction of all these processes makes it hard to have a clear idea
what is going on.