Abstract
ObsSlice is an optimization tool suited for the verification of timed automata using virtual observers. It discovers the set of modelling elements that can be safely ignored at each location of the observer by synthesizing behavioral dependence information among components. ObsSlice is fed with a network of timed automata and generates a transformed network which is equivalent to the one provided up to branching-time observation. Preliminary results have proven that eliminating irrelevant activity mitigates state space explosion and has a positive -and sometimes dramatic- impact on the performance of verification tools in terms of time, size and counterexample length.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Braberman, V., Garbervetsky, D., Olivero, A.: Improving the verification of timed systems using influence information. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 21. Springer, Heidelberg (2002)
Alfonso, A., Braberman, V., Kicillof, N., Olivero, A.: Visual timed event scenarios. In: Proc. of the 26th ACM/IEEE ICSE 2004, to appear (2004)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The Tool KRONOS. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)
Tripakis, S.: L’Analyse Formelle des Systemès Temporisés en Practique. PhD thesis, Univesité Joseph Fourier (1998)
Behrmann, G., David, A., Larsen, K., Möller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. IEEE CDC 2001, IEEE Computer Society Press, Los Alamitos (2001)
Braberman, V., Felder, M.: Verification of real-time designs: Combining scheduling theory with automatic formal verification. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, p. 494. Springer, Heidelberg (1999)
Braberman, V.: Modeling and Checking Real-Time Systems Designs. PhD thesis, FCEyN, Universidad de Buenos Aires (2000)
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
Braberman, V., Garbervetsky, D., Olivero, A. (2004). ObsSlice: A Timed Automata Slicer Based on Observers. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_39
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive