A logic programming based specification animation tool for real-time systems

During the elicitation and verification of the specification for real-time control systems, the sequential-temporal aspects need to be treated separately. These aspects also require animation for verification and incremental refinement of the specification. An automated tool kit can be used to mechanize animation of specification. An augmented Petri net modeling tool is adopted to capture the logical, sequential and timing dependencies of a real-time control system. A description is also given of a logic-programming-based animator for automated animation of the Petri net description. The augmentations involve a predicate net approach and temporal extensions