Verifying time-bounded properties for ELECTRE reactive programs with stopwatch automata

1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. IEEE 5th Symp. Logic in Computer Science, 1990.

   Google Scholar 

2. R. Alur, C. Courcoubetis, T.A Henzinger, and P. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Proc. Workshop on Theory of Hybrid Systems, 1993.

   Google Scholar 

3. Albert Benveniste and Gérard Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9):1270–1282, September 1991.

   Google Scholar 

4. Frédéric Boussinot and Robert De Simone. The Esterel language. Proceedings of the IEEE, 79(9):1293–1304, September 1991.

   Google Scholar 

5. F. Cassez and O. Roux. Compilation of the Electre reactive language into finite transition systems. Theoretical Computer Science, 144, June 1995. to appear.

   Google Scholar 

6. Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous dataflow language Lustre. Proceedings of the IEEE, 79(9):1304–1320, September 1991.

   Google Scholar 

7. T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata. To appear, 1995.

   Google Scholar 

8. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic modelchecking for real-time systems. In Proc. IEEE 7th Symp. Logic in Computer Science, 1992.

   Google Scholar 

9. David Harel and Amir Pnueli. On the development of reactive systems. In K.R. Apt, editor, Logics and Models of Concurrent Systems, volume 13, pages 477–498. NATO ASI Series, (Springer Verlag, New-York), 1985.

   Google Scholar 

10. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Proc. Workshop on Theory of Hybrid Systems, 1993.

    Google Scholar 

11. Paul Le Guernic, Michel Le Borgne, Thierry Gautier, and Claude Le Maire. Programming real-time applications with Signal. Proceedings of the IEEE, 79(9):1321–1336, September 1991.

    Google Scholar 

12. X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In Proc. Workshop on Theory of Hybrid Systems, 1993.

    Google Scholar 

13. X. Nicollin, J. Sifakis, and S. Yovine. Compiling real-time specifications into extended automata. IEEE Transactions on Software Engineering, 18(9):794–804, 1992.

    Google Scholar 

14. J. Perraud, O. Roux, and M. Huou. Operational semantics of a kernel of the language Electre. Theoretical Computer Science, 97(1):83–104, april 1992.

    Google Scholar 

15. A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. In Proc. Conference on Computer-Aided Verification, 1994.

    Google Scholar 

16. O. Roux and V. Rusu. Verifying real-time systems with decidable hybrid automata. In Second European Workshop on Real-Time and Hybrid Systems, 1995.

    Google Scholar 

17. H. Le Verge. A note on chernikova's algorithm. Technical report, 437, IRISA, Rennes, France, 1992.

    Google Scholar 

18. D.K. Wilde. A library for doing polyhedral operations. Technical report, 2157, IRISA, Rennes, France, 1993.

    Google Scholar 

19. S. Yovine. Méthodes et outils pour la vérification symbolique de systèmes temporisĒs. PhD thesis, Institut National Polytechnique de Grenoble, 1993.

    Google Scholar 

Download references