Modeling and Verification of Network Protocol Specs using Timed Pi-Calculus
We present a toolkit based on our timed extension of pi-calculus. The calculus is employed as a domain specific language for modeling telecommunication protocols with real-time properties. This model can be simulated, visualized, debugged and transformed for model-checking using UPPAAL. This paper introduces the general structure of our toolkit and provides a unified running example. Index Terms-timed pi-calculus, simulation, verification, telecommunication protocols
Author
Kamal Barakat and Stefan Kowalewski