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.