Specification and simulation of a concurrent real-time system

Interval Temporal Logic (ITL) is real-time logic for specifying and verifying real-time systems. In this paper, ITL is used to specify a concurrent realtime system: assembly line which is an abstract model of industrial robot control systems. We can specify the abstract properties of the system in ITL as well as the system design using the executable subset of ITL, Tempura. Comparing with other approaches, the first advantage of this methodology is that the concurrent real-time systems can be naturally specified in true concurrent model rather than interleaving model. The second is that the specification of system design is executable so that the simulation can be obtained in the same formal framework. Therefore, both the properties of the system and the consistency of specification can be checked before verification.