A Native Approach to Modeling Timed Behavior in the Pi-Calculus

We introduce a new concept of modeling timed behavior in pi-calculus by representing timed actions (or timers) as interactions between application processes and clock processes. This approach extends the original calculus in a manner such that bisimulation arrangements in pi-calculus remain untouched. We also present a tool to simulate specifications written in our timed version of pi-calculus in order to verify their behavior.