A Verification Framework for Time-Triggered Networks Based on Timed Colored Petri Net

Published In

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Document Type

Citation

Publication Date

2023

Abstract

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.

DOI

10.1109/TCAD.2024.3355708

Persistent Identifier

https://archives.pdx.edu/ds/psu/41255

Publisher

IEEE

Share

COinS