×

Speeding up model checking of timed-models by combining scenario specialization and live component analysis. (English) Zbl 1262.68104

Ouaknine, Joël (ed.) et al., Formal modeling and analysis of timed systems. 7th international conference, FORMATS 2009, Budapest, Hungary, September 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04367-3/pbk). Lecture Notes in Computer Science 5813, 58-72 (2009).
Summary: 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.
For the entire collection see [Zbl 1176.68014].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Kronos; Uppaal
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L., Burgueño, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998) · doi:10.1007/BFb0054177
[2] Alpern, B., Schneider, F.: Verifying temporal properties without temporal logic. ACM Trans. Programming Lang. and Systems 11(1), 147–167 (1989) · Zbl 0676.68003 · doi:10.1145/59287.62028
[3] Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993) · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[4] Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[5] Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003) · Zbl 1031.68076 · doi:10.1007/3-540-36577-X_18
[6] Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Proceedings of the International Conference on Hybrid Systems, pp. 232–243. Springer, Heidelberg (1995)
[7] 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, vol. 1427, pp. 546–550. Springer, Heidelberg (1998) · doi:10.1007/BFb0028779
[8] Braberman, V.: Modeling and Checking Real-Time Systems Designs. PhD thesis, FCEyN. Univ. de Buenos Aires (2000)
[9] 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
[10] Braberman, V.A., 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, pp. 21–36. Springer, Heidelberg (2002) · Zbl 1043.68588 · doi:10.1007/3-540-46002-0_3
[11] 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, vol. 3114, pp. 470–474. Springer, Heidelberg (2004) · Zbl 1103.68608 · doi:10.1007/978-3-540-27813-9_39
[12] Braberman, V., Kicillof, N., Olivero, A.: A scenario-matching approach to the description and model checking of real-time properties. IEEE Transactions on Software Engineering 31(12), 1028–1041 (2005) · Zbl 05114774 · doi:10.1109/TSE.2005.131
[13] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
[14] Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proceedings of IEEE RTSS 1996. IEEE Computer Society Press, Los Alamitos (1996)
[15] Grieskamp, W., Kicillof, N., Tillmann, N.: Action machines: A framework for encoding and composing partial behaviors. Int. Jour. SEKE 16(5), 705–726 (2006)
[16] Harel, D., Marelly, R.: Playing with time: On the specification and execution of time-enriched LSCs. In: Proceedings of the 10th IEEE/ACM International Symposium MASCOTS 2002, pp. 193–202. IEEE Computer Society Press, Los Alamitos (2002)
[17] Kugler, H.-J., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal Logic for Scenario-Based Specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005) · Zbl 1087.68596 · doi:10.1007/978-3-540-31980-1_29
[18] Ledru, Y., du Bousquet, L., Bontron, P., Maury, O., Oriat, C., Potet, M.-L.: Test purposes: Adapting the notion of specification to testing. In: Proceedings of the 16th IEEE Int. Conf. ASE 2001. IEEE Computer Society Press, Los Alamitos (2001)
[19] Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: SIGSOFT FSE, pp. 167–176 (2002) · doi:10.1145/587051.587077
[20] Zheng, T., Khendek, F., Parreaux, B.: Refining timed mscs. In: Reed, R., Reed, J. (eds.) SDL 2003. LNCS, vol. 2708, pp. 234–250. Springer, Heidelberg (2003) · Zbl 1038.68937 · doi:10.1007/3-540-45075-0_14
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.