Formal Specification, Verification and Simulation of Time-Dependent Systems: a Timed Process Algebra Approach

Abstract In this paper, we present an approach to specification, verification and validation of concurrent time-dependent systems which is centered on a timed process algebra language, called RTL (for real time LOTOS). Our approach is supported by a tool named RTL-Analyzer, that allows automatic verification and validation of RTL specifications. RTL is a temporal extension of basic LOTOS language which expresses and handles temporal constraints associated with actions. First, we present and justify the use of RTL to specify concurrent time-dependent systems. Then, the main characteristics and functionalities of the RTL-Analyzer are presented with details for systems verification and validation using our approach. An example of a time-dependent system is given and it is specified and analyzed by our tool. Finally, we compare our approach with others proposed in the literature.