A method for modeling and verification of real-time systems

Real-time systems are used in many critical applications. Verification of these real-time systems is essential. Presented here is a method for modeling real-time systems and computing the model's timing characteristics automatically. From a data-driven model of the system an equivalent finite state machine representation of the system is produced by this package. To provide efficient traversal of this large state space an Ordered Binary Decision Diagram (OBDD) is used to represent the state machine using symbolic methods. Algorithms have been developed to find the largest and smallest distance (times) between any two state sets. From these algorithms schedulability of the real-time system can be determined.