Reachability analysis of real-time systems using time Petri nets.

Area of Science:

• Computer Science
• Formal Methods
• Real-Time Systems

Background:

• Time Petri Nets (TPNs) are widely used for real-time system specification and verification.
• Traditional reachability analysis for TPNs has limitations in verifying timing properties like end-to-end delays.
• Existing methods do not adequately support the derivation of task execution delays crucial for time-critical systems.

Purpose of the Study:

• To present a novel reachability-based analysis technique for TPNs.
• To enable effective timing property analysis and verification, specifically addressing end-to-end delay computation.
• To offer a more general analysis method compared to existing techniques.

Main Methods:

• Development of a new analysis technique based on clock-stamped state classes (CS-classes).
• Construction of a reachability tree using CS-classes to facilitate direct end-to-end delay computation.
• Demonstration of the technique's applicability to command and control (C2) systems.

Main Results:

• The proposed CS-class-based reachability analysis allows direct computation of end-to-end task execution delays.
• CS-classes can be mapped to traditional state classes, indicating the technique's generality.
• The method effectively addresses limitations of existing TPN reachability analysis for timing properties.

Conclusions:

• The CS-class-based technique provides a more general and effective approach for timing property verification in TPNs.
• This method enhances the analysis of real-time systems by enabling direct calculation of critical timing parameters.
• The technique is demonstrated to be applicable to complex systems like command and control architectures.