We consider the problem of verifying invariance properties for duration systems. Such systems are (extended) timed graphs with duration variables. They are especially suitable for describing real time schedulers. However, for this kind of systems, the verification problem of invariance properties is in general undecidable. We propose an over approximation method based on a particular extension of a given duration system, and we show that our over approximation includes all the digitization of all the real computations of the duration system. The over-approximated system can then be used to perform an interesting close analysis of invariance properties of the initial system, while other existing approaches fail.

[1] Alur R. and Dill D., “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.

[2] Alur R. and Dill D., “Automata for Modeling Real Time Systems,” in Proceedings of International Colloquium on Automata and Programming (ICALP'90), Warwick, 1990.

[3] Alur R., Courcoubetis C., and Dill D., “Model Checking for Real-Time Systems,” in Proceedings of 5th Symposium on Logic in Computer Science (LICS'90), Philadelphia, USA, 1990.

[4] Alur R., Courcoubetis C., Henzinger T., and Ho P. H., “Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems,” in Proceedings of Hybrid Systems, Springer-Verlag, 1993.

[5] Alur R., Courcoubetis C., Halbwatchs N., Henzinger T. A., Ho P. H., Nicollin X., Olivero A., Sifakis J., and Yovine S., “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, pp. 3- 34, 1995. On the Verification by Approximation of Duration Systems 155

[6] Bouajjani A. and Robbana R., “Verifying w- Regular Properties for Subclasses of Linear Hybrid Systems,” in Proceedings of Computer- Aided Verification (CAV'95), Belgium, 1995.

[7] Bouajjani A., Echahed R., and Robbana R., “On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures,” in Proceedings of Hybrid Systems and Autonomous Control, New York, USA, 1995.

[8] Bouajjani A., Enchahed R., and Robbana R., “Verifying Invariance Properties of Timed Systems with Duration Variables,” in Proceedings of Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFTS'94), 1994.

[9] Bouajjani A., Echahed R., and Robbana R., “Verification of Context-Free Timed Systems Using Linear Hybrid Observers,” in Proceedings of Computer-Aided Verification (CAV'94), USA, 1994.

[10] Bouajjani A., Lakhnech Y., and Robbana R., “From Duration Calculus to Linear Hybrid Systems,” in Proceedings of Computer-Aided Verification (CAV'95), Belgium, 1995.

[11] Cerans K., “Decidability of Bisimulation Equivalence for Parallel Timer Processes,” in Proceedings of Computer-Aided Verification (CAV'92), Montreal, Canada, 1992.

[12] Chaochen Z., Hoare R., and Ravn P., “A Calculus of Durations,” Information Processing Letters, vol. 40, pp. 269-276, 1991.

[13] Frank C. and Kim L., “The Impressive Power of Stopwatches,” in Proceedings of Conference on Concurrency Theory (CONCUR'00), Pennsylvania, USA, 2000.

[14] Henzinger A., Kopke W., Puri A., and Varaiya P., “What's Decidable about Hybrid Automata?,” Journal of Computer and System Science, vol. 57, pp. 94-124, 1998.

[15] Henzinger A., Manna Z., and Pnuelli A., “What Good are Digital Clocks?,” in Proceedings of International Colloquium on Automata Languages and Programming, 1992.

[16] Henzinger A., Nicollin X., Sifakis J., and Yovine S., “Symbolic Model-Checking for Real Time Systems,” in Proceedings of 7 th Symposium on Logic in Computer Science (LICS'92), Santa Cruz, USA, 1992.

[17] Kesten Y., Pnueli A., Sifakis J., and Yovine S., “Decidable Integration Graphs,” Information and Computation, vol. 150, no. 2, pp. 209-243, 1999.

[18] Kesten Y., Pnueli A., Sifakis J., and Yovine S., “Integration Graphs: A Class of Durable Hybrid Systems,” in Proceedings of Hybrid Systems, Springer Verlag, 1993.

[19] Nicollin X., Olivero A., Sifakis J., and Yovine S., “An Approach to the Description and Analysis of Hybrid Systems,” in Proceedings of Hybrid Systems, Springer-Verlag, 1993.

[20] Pnueli A. and Shahar E., “Liveness and Acceleration in Parameterized Verification,” in Proceedings of Computer-Aided Verification (CAV'00), Chicago, USA, 2000.

[21] Robbana R., “Réduction et Vérification de Systèmes Temps-Réel Distribués,” in Colloque Francophone de l'Ingénierie des Protocoles (CFIP'99), Nancy, France, 1999.

[22] Robbana R., “Verification of Duration Systems Using an Approximation Approach,” Journal of Computer Science and Technology, vol. 18, no. 2, pp.153-162, 2003

[23] Robbana R., “Verification of Integrated Timed Systems,” in Proceedings of Maghrebian Conference on Software Engineering (MCSEA'98) and Artificial Intelligence, Tunis, 1998. Narjes Berregeb received an engineering degree in computer science from the Faculty of Sciences of Tunis in 1992, and a PhD degree in computer science on automatic proofs by induction in associative commutative and observational theories from Henri Poincaré University at Nancy. Currently, she is a lecturer at the Institut National des Sciences Appliquées et de Technologie at Tunis. Her research interests include theorem proving techniques and formal methods for specification and verification. Riadh Robbana received an engineering degree in computer science from the Faculty of Sciences of Tunis in 1991, and a PhD degree in computer science on hybrid systems verification from Joseph Fourier University at Grenoble. Currently, he is a lecturer and head of the Department of Applied Mathematics and Computer Science at Ecole Polytechnique of Tunisia. His research interests include formal verification of real-time systems.