Model Checking of Credit Setting in AFDX Traffic Policing
Huagang Xiong · Aeronautical Computing Technique · 2011
In the Avionics Full Duplex Switched Ethernet(AFDX) real-time communications,credited token buckets are applied in switched nodes for traffic policing.Test automata are designed for bounded liveness model checking under concurrent interaction scenarios with the time automata models,which are built for the frame-based and byte-based credited token buckets respectively.According to the formal verification,it′s shown that latency jitters in multiplexer output queuing are limited by traffic policing with burstiness constraints.However,jitters of input virtual links(VL) should also be considered when setting the credit values;otherwise,the greater jitter values may be caused by disturbing aggregated frames belong to different VLs.By analyzing the inter-relations of credit setting and jitters,some notes are summarized for traffic policing configurations.