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.