Special Session on
Formal Verification of Telecommunications Systems

organized by
Tatjana Kapus, University of Maribor, Slovenia
Gordan Jezic, University of Zagreb, Croatia

Telecommunications systems have several characteristics which make them difficult to design and test. They are inherently concurrent, distributed, reactive, and operate in real-time. They are usually huge in terms of software code size, have a large number of participating objects, and last but not least, they have a large number of end users, which expect high reliability, availability, and correct operation of provided services.

The system design complexity increases due to the convergence of Internet-type data communications and traditional telecommunications, as well as different kinds of mobility, and consequently, the constantly increasing diversity of services. Thus, it is very important that design errors are detected early in the telecommunications system design cycle.

Formal verification is a method which takes the formal description of a system (part) and the formal specification of correctness requirements, and proves - or disproves - that the system satisfies them. Whereas the use of some formal and semi-formal languages (e.g. SDL, UML, MSC) is quite well established in the telecommunications industry, the use of (non-exhaustive) simulation and testing largely prevails over the use of formal verification techniques. It is generally agreed that formal verification cannot substitute simulation and testing, however, it could be used as a supplementary method to assure at least correctness with respect to some correctness criteria and/or for some system parts.

The main objective of this special session is to discuss and/or demonstrate the use of formal verification in industrial telecommunications system design. We would like to hear to what extent formal verification is used in the telecommunications industry and what is being done to make its use more common. With this objective in mind, we primarily solicit original submissions on the application of formal verification in industrial projects and on new methods and tools for enabling such applications. We also welcome submissions related to the use of formal verification in telecommunications system design.

Here is a non-exhaustive list of topics:

• industrial case studies
• automated formal verification
• formal verification using exhaustive simulation
• model checking
• theorem proving
• formal verification of protocols and services
• formal verification of mobile systems
• formal verification of logical correctness and real-time properties
• feature interaction detection using formal verification
• formal verification of software code
• test case generation using formal verification
• formal languages for design and requirement specification

All papers will go through a regular review process, coordinated by the special session organizer(s).

Should you have further questions, please contact either of the session organizers:

Dr. Tatjana Kapus FERI, University of Maribor Smetanova ul. 17 SI-2000 Maribor, Slovenia E-mail: kapus@uni-mb.si Phone: +386 2 220 7213 Fax: +386 2 251 1178

Dr. Gordan Jezic FER, University of Zagreb Unska 3 HR-10000 Zagreb, Croatia E-mail: gordan.jezic@fer.hr Phone: +385 1 6129 825 Fax: +385 1 6129 832

[ back to list of special sessions ]