Safety analysis in real-time system using constraint logic programming

This paper is concerned with the verification of the timing safety properties of real-time systems. Using CLP (BNR) Prolog, we show how constraint logic programming based on relational interval arithmetic can provide a much simpler analysis technique than some previous graph-theoretic approaches to the problem of verifying a timing property with respect to a system specification. Both the property and the system to verify are specified by formulas in subsets of Real Time Logic. In particular, our new approach will allow more complex timing behaviours, such as delay correlation, to be considered in the timing models.