Vérification symbolique pour les protocoles de communication
Dorel Marius Bozga · HAL (Le Centre pour la Communication Scientifique Directe) · 1999
The use of formal methods for the design of telecommunication protocols is recognized from now on to be the only approach able to guarantee their correct operation before the startup. However, always increasing complexity as well as severe reliability and safety constraints require the extension of the description formalisms and the continuous improvement of validation techniques and tools. This thesis defines an intermediate representation, named IF, for the description of protocols. IF is built based on communicating timed automata with deadlines. The deadlines allow the explicit modeling of the urgency of the actions and are a very fine means to describe the temporal evolution of a system. The automata communicate either in an asynchronous way, by fifo queues, or in a synchronous way by rendez-vous. An operational semantics for IF is formally defined and efficient simulation techniques are proposed. Moreover, having a static structure, IF allows the intensive application of static analysis, such as those resulting from the field of the compiler code optimization. Some of the information computed by static analysis can improve considerably the performances of the automatic validation. An open validation platform was installed around IF. It integrates a great number of tools as much academic than industrial and covers the majority of techniques currently employed for the verification and the test of protocols. This platform was successfully used on real communications protocols, such as SSCOP or STARI.