Formal verification invariance properties of a robot sheet metal pressing cell

This paper shows that logic programming languages, such as PROLOG, provide useful computational logic for modelling, simulating and verifying real-time discrete event processes. The notion of a timed transition model (TTM) is provided as a generic computational model for real-time systems and real-time temporal logic (RTTL) is used for specifying the properties to be verified. Automatic testing and simulation of safety properties of the system specification by the logic programming language PROLOG is presented using the example of a simplified TTM press line model. Interest is limited to the use of PROLOG in the construction and checking of proof diagrams for the time invariance of system specifications.