An Approach to Protocol Modeling and Validation

This paper describes an approach to modeling and analysis of complex time-dependent systems specified by modular Time Petri Nets (TPNs). The approach is supported by a Java tool TPN DESIGNER- which permits visual modeling, debugging and discrete-event simulation. The tool is characterized by its modularity and hierarchical constructs, a scripting language for controlling model configuration and scalability, and a monitoring and watching sub system for collecting simulation output. TPN DESIGNER permits also to split a model into LP/subnets for distributed simulation. The tool is able to translate a flattened TPN model into UPPAAL/Timed Automata for model checking. The paper demonstrates the practical use of the approach through modeling and validation of a system based on the alternating bit protocol.