Prof. Ing. Tomáš Vojnar, Ph.D.

ADVANCE -- Advanced Validation Techniques for Telecommunication Protocols

Reseach leader:Bouajjani Ahmed (UPAR7)
Team members:Matoušek Petr, Vojnar Tomáš
Agency:The Information Society Technologies (IST) programme of the EU Fifth Framework Programme
Code:IST-1999-29082
Start:2001-10-01
End:2004-01-31
Project description:
Telecommunication protocols are critical systems of very high complexity. The goal of the project is to develop a new generation of validation tools based on advanced and novel techniques allowing to tackle problems that arise in the validation of modern protocols, and that are beyond the scope of the state-of-the-art methods and tools. The objectives of this project are (1) to develop a general methodology for the specification and automated validation of telecommunication protocols, taking into account important aspects such as: complex timing constraints, use of unbounded data structures like counters and queues, parametrization, mobility, etc. (2) to provide tool support for this methodology, and (3) to prove it substantially advances the state of the art by applying it to industrially relevant case studies. Experience shows that the verification of realistic systems cannot be achieved without applying a tight combination of several approaches and analysis techniques. We are convinced that the next generation validation tools should be built by embedding several specialized tools in a single framework. These tools should apply complementary approaches and be able to communicate and cooperate easily. The goal of our project is to produce such a framework. Our approach consists of a combination of powerful abstraction techniques, and efficient validation procedures based on reachability analysis of finite and infinite-state systems. These techniques are embedded in a common formal framework based on the model of extended automata, i.e., automata with data structures. All usual models are particular instances of this general model.

Publications

2007VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6.
2004BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science. 2004, vol. 2004, no. 3114, pp. 372-386. ISSN 0302-9743.
 MATOUŠEK Petr and SIGHIREANU Mihaela. Parametric Analysis of PGM protocol. Advance meeting, Paris, 2004.
 MATOUŠEK Petr. A New Data Structure Based on Intervals. In: Proceedings of MOVEP'04. Bruxelles, 2004, pp. 16-21.
 MATOUŠEK Petr. Tools for Parametric Verification. A Comparison on a Case Study. Journal of Universal Computer Science. 2004, vol. 10, no. 10, pp. 1469-1495. ISSN 0948-6968.
 MATOUŠEK Petr. Tools for Parametric Verification: A Comparison on a Case Study. In: Proceedings of the 5th Joint Workshop on FSCBS. Stirling: University of Stirling, 2004, pp. 45-55. ISBN 1-85769-197-0.
2003BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. Lecture Notes in Computer Science. 2003, vol. 2003, no. 2761, pp. 174-190. ISSN 0302-9743.
2002BOUAJJANI Ahmed and VOJNAR Tomáš. Automata with Parameterized Arrays and Parameterized Networks of Automata. Paris: The Information Society Technologies (IST) programme of the EU Fifth Framework Programme, 2002.
 BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Verification of Parameterized Concurrent Systems with Resource Sharing. Paris: The Information Society Technologies (IST) programme of the EU Fifth Framework Programme, 2002.

Your IPv4 address: 54.163.209.109
Switch to IPv6 connection

DNSSEC [dnssec]