Abstract
We present ELSE, a new state generator for timed automata. ELSE is based on VERIMAG’s IF-2.0 specification language and is designed to be used with state exploration tools like CADP. In particular, it compiles IF-2.0 specifications to C programs that link with CADP. It thus concentrates on the generation of comparatively small state spaces and integrates into existing tool chains. The emphasis of the ELSE development is on fundamentally different data structures and algorithms, notably on the level of zones. Rather than representing possible values of clocks at a given symbolic state, event zones represent in an abstract way the timing constraints of past and future events.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: An intermediate representation and validation environment for timed asynchronous systems. World Congress on Formal Methods (1), 307–327 (1999)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)
Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W., Lind-Nielsen, J.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)
D’Souza, D., Thiagarajan, P.S.: Distributed interval automata: A subclass of timed automata, Internal Report TCS-98-3 (1998)
Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: IEE Real-Time Systems Symposium, pp. 73–81 (December 1996)
Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032, Springer, Heidelberg (1996)
Lugiez, D., Niebert, P., Zennou, S.: Clocked mazurkiewicz traces for partial order reductions of timed automata, draft (2003), available at http://www.cmi.univ-mrs.fr/~niebert/docs/clockedmazu.pdf
Larsen, K., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)
Minea, M.: Partial order reduction for verification of timed systems, Ph.D. thesis, Carnegie Mellon University (1999)
Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Yoneda, T., Schlingloff, B.-H.: Efficient verification of parallel real-time systems. Formal Methods in System Design 11(2), 197–215 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zennou, S., Yguel, M., Niebert, P. (2004). ELSE: A New Symbolic State Generator for Timed Automata. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive