Navegar

Colección

Datos Estadísticas

Artículo

Braberman, V.; Garbervestky, D.; Kicillof, N.; Monteverde, D.; Olivero, A. "Speeding up model checking of timed-models by combining scenario specialization and live component analysis" (2009) 7th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2009. 5813 LNCS:58-72
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

The common practice for verifying properties described as event occurrence patterns is to translate them into observer state machines. The resulting observer is then composed with (the components of) the system under analysis in order to verify a reachability property. Live Component Analysis is a "cone of influence" abstraction technique aiming at mitigating state explosion by detecting, at each observer location, which components are actually relevant for model checking purposes. Interestingly enough, the more locations the observer has, the more precise the relevance analysis becomes. This work proposes the formal underpinnings of a method to safely leverage this fact when properties are stated as event patterns (scenarios). That is, we present a sound and complete method of property manipulation based on specializing and complementing scenarios. The application of this method is illustrated on two case studies of distributed real-time system designs, showing dramatic improvements in the verification phase, even in situations where verification of the original scenario was unfeasible. © 2009 Springer Berlin Heidelberg.

Registro:

Documento: Artículo
Título:Speeding up model checking of timed-models by combining scenario specialization and live component analysis
Autor:Braberman, V.; Garbervestky, D.; Kicillof, N.; Monteverde, D.; Olivero, A.
Ciudad:Budapest
Filiación:FCEyN, UBA, Argentina
Microsoft, United States
INTEC, UADE, Argentina
ECyT, UNSAM, Argentina
Palabras clave:Abstraction techniques; Component analysis; Distributed real time system; Event pattern; Occurrence pattern; Reachability; State explosion; State machine; Location; Object oriented programming; Real time systems; Time sharing systems; Model checking
Año:2009
Volumen:5813 LNCS
Página de inicio:58
Página de fin:72
DOI: http://dx.doi.org/10.1007/978-3-642-04368-0-7
Título revista:7th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2009
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5813LNCS_n_p58_Braberman

Referencias:

  • Aceto, L., Burgueno, A., Larsen, K.G., Model checking via reachability testing for timed automata (1998) LNCS, 1384, pp. 263-280. , Steffen, B, ed, TACAS 1998, Springer, Heidelberg
  • Alpern, B., Schneider, F., Verifying temporal properties without temporal logic (1989) ACM Trans. Programming Lang. and Systems, 11 (1), pp. 147-167
  • Alur, R., Courcoubetis, C., Dill, D.L., Model-checking in dense real-time (1993) Information and Computation, 104 (1), pp. 2-34
  • Alur, R., Dill, D.L., A theory of timed automata (1994) Theoretical Computer Science, 126 (2), pp. 183-235
  • Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G., Static guard analysis in timed automata verification (2003) LNCS, 2619, pp. 254-270. , Garavel, H, Hatcliff, J, eds, TACAS 2003, Springer, Heidelberg
  • Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., UPPAAL - a tool suite for automatic verification of real-time systems (1995) Proceedings of the International Conference on Hybrid Systems, pp. 232-243. , Springer, Heidelberg
  • Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, 1427, pp. 546-550. Springer, Heidelberg (1998); Braberman, V., (2000) Modeling and Checking Real-Time Systems Designs, , PhD thesis, FCEyN. Univ. de Buenos Aires
  • Braberman, V., Garbervetsky, D., Kicillof, N., Monteverde, D., Olivero, A.: Specializing scenarios. Technical report, DC. FCEN. UBA (2008), http://www.dc.uba.ar/people/exclusivos/vbraber; Braberman, V.A., Garbervetsky, D., Olivero, A., Improving the verification of timed systems using influence information (2002) LNCS, 2280, pp. 21-36. , Katoen, J.-P, Stevens, P, eds, TACAS 2002, Springer, Heidelberg
  • Braberman, V.A., Garbervetsky, D., Olivero, A.: ObsSlice: A timed automata slicer based on observers. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, 3114, pp. 470-474. Springer, Heidelberg (2004); Braberman, V., Kicillof, N., Olivero, A., A scenario-matching approach to the description and model checking of real-time properties (2005) IEEE Transactions on Software Engineering, 31 (12), pp. 1028-1041
  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , MIT Press, Cambridge
  • Daws, C., Yovine, S., Reducing the number of clock variables of timed automata (1996) Proceedings of IEEE RTSS, , IEEE Computer Society Press, Los Alamitos
  • Grieskamp, W., Kicillof, N., Tillmann, N., Action machines: A framework for encoding and composing partial behaviors (2006) Int. Jour. SEKE, 16 (5), pp. 705-726
  • Harel, D., Marelly, R., Playing with time: On the specification and execution of time-enriched LSCs (2002) Proceedings of the 10th IEEE/ACM International Symposium MASCOTS, pp. 193-202. , IEEE Computer Society Press, Los Alamitos
  • Kugler, H.-J., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y., Temporal Logic forScenario-Based Specifications (2005) LNCS, 3440, pp. 445-460. , Halbwachs, N, Zuck, L.D, eds, TACAS 2005, Springer, Heidelberg
  • Ledru, Y., du Bousquet, L., Bontron, P., Maury, O., Oriat, C., Potet, M.-L., Test purposes: Adapting the notion of specification to testing (2001) Proceedings of the 16th IEEE Int. Conf. ASE, , IEEE Computer Society Press, Los Alamitos
  • Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: SIGSOFT FSE, pp. 167-176 (2002); Zheng, T., Khendek, F., Parreaux, B.: Refining timed mscs. In: Reed, R., Reed, J. (eds.) SDL 2003. LNCS, 2708, pp. 234-250. Springer, Heidelberg (2003)

Citas:

---------- APA ----------
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D. & Olivero, A. (2009) . Speeding up model checking of timed-models by combining scenario specialization and live component analysis. 7th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2009, 5813 LNCS, 58-72.
http://dx.doi.org/10.1007/978-3-642-04368-0-7
---------- CHICAGO ----------
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A. "Speeding up model checking of timed-models by combining scenario specialization and live component analysis" . 7th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2009 5813 LNCS (2009) : 58-72.
http://dx.doi.org/10.1007/978-3-642-04368-0-7
---------- MLA ----------
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A. "Speeding up model checking of timed-models by combining scenario specialization and live component analysis" . 7th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2009, vol. 5813 LNCS, 2009, pp. 58-72.
http://dx.doi.org/10.1007/978-3-642-04368-0-7
---------- VANCOUVER ----------
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A. Speeding up model checking of timed-models by combining scenario specialization and live component analysis. Lect. Notes Comput. Sci. 2009;5813 LNCS:58-72.
http://dx.doi.org/10.1007/978-3-642-04368-0-7