Time-triggered (TT) network provides a low-cost service to meet the strong demand of modern industry networks for real-time communication. Both simulation and reachability analysis provide effective research methods for TT networks. This paper presents a verification framework for the TT network based on Timed Colored Petri Nets (TCPN). We propose an automatic formal modeling method for the behavior of message transmissions in the TT network. We harness timed multisets of TCPN to model and analyze time-triggered message transmission latencies. For a holistic system evaluation, we characterize the critical system properties such as boundedness and liveness. We substantiate the properties by the reachability analysis. We demonstrate the effectiveness through a case study by simulating the message transmission and reachability analysis in the state space. Finally, we analyze the influencing factors of the state space in the automotive scenario. The proposed automatic modeling method can effectively reduce the state space scale.

Modeling and testing for a parallel software system is very difficult, because parallel behaviors leads to system state explosion. Many testing methods are testing with a large number of redundancies. In this paper, a test sequence selection method for parallel software systems is shown. The method is based on linear behavior sequences which is preparing for testing, called LBSPT. Firstly, a formal model for software system specification is constructed based on Coloured Petri Net (CPN), called system model, and LBSPT is also modeled based on CPN, called LBSPT model. A test sequence selection method is defined on these models. The method could select all of test sequences related to LBSPT, and does not contain any redundancy. The state explode problem in software testing is solved to a certain extent. Practices show that the effect of this method is better than other methods such as random walk.

Hierarchical mobile management is designed to improve the performance of original Mobile IPv6 protocol. However, such improvements also introduce more complicated protocol behaviors. In order to effectively analyze the functionalities of this protocol, formal methods should be adopted. In this paper, a Colored Petri Nets (CPN) based formal model of Hierarchical Mobile IPv6 (HMIPv6) protocol is proposed. Then, simulation and state space analysis are utilized to validate the model and verify some higher functional properties of HMIPv6 protocol. The proposed formal model could not only be served as an unambiguous and visual formal specification of HMIPv6 protocol, but also facilitate protocol behavior simulation and properties analysis.