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.
Citation:
F. Cicirelli, A. Furfaro,, L. Nigro, "An Approach to Protocol Modeling and Validation," anss, pp.261-268, 39th Annual Simulation Symposium (ANSS'06), 2006