×

An incremental and modular technique for checking LTL\(\setminus \)X properties of Petri nets. (English) Zbl 1215.68155

Derrick, John (ed.) et al., Formal techniques for networked and distributed systems – FORTE 2007. 27th IFIP WG 6.1 international conference, Tallinn, Estonia, June 27–29, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73195-5/pbk). Lecture Notes in Computer Science 4574, 280-295 (2007).
Summary: Model-checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. Modular verification is a promising natural approach to tackle this problem. It is based on the “divide and conquer” principle and aims at deducing the properties of the system from those of its components analysed in isolation. Unfortunately, several issues make the use of modular verification techniques difficult in practice. First, deciding how to partition the system into components is not trivial and can have a significant impact on the resources needed for verification. Second, when model-checking a component in isolation, how should the environment of this component be described? In this paper, we address these problems in the framework of model-checking LTL\(\setminus \)X action-based properties on Petri nets. We propose an incremental and modular verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account using the linear place invariants of the system.
For the entire collection see [Zbl 1119.68006].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Cadence SMV
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bhat, G., Peled, D.: Adding partial orders to linear temporal logic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 119–134. Springer, Heidelberg (1997) · Zbl 0930.68063 · doi:10.1007/3-540-63141-0_9
[2] Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992) · doi:10.1145/136035.136043
[3] Christensen, S., Petrucci, L.: Søren Christensen and Laure Petrucci. Computer Journal 43(3), 224–242 (2000) · Zbl 0960.68125 · doi:10.1093/comjnl/43.3.224
[4] Cobleigh, J., Giannakopoulou, D., Pasareanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, Springer, Heidelberg (2003) · Zbl 1031.68545 · doi:10.1007/3-540-36577-X_24
[5] Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 253–271. Springer, Heidelberg (1999) · Zbl 0954.68102 · doi:10.1007/3-540-48119-2_16
[6] Couvreur, J.-M.: A bdd-like implementation of an automata package. In: CIAA 2004. LNCS, vol. 3317, pp. 310–311. Springer, Heidelberg (2004) · Zbl 1115.68425
[7] Geldenhuys, J., Valmari, A.: Techniques for smaller intermediary bdds. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 233–247. Springer, Heidelberg (2001) · Zbl 1006.68097 · doi:10.1007/3-540-44685-0_16
[8] Girault, C., Valk, R.: Petri Nets for Systems Engineering – A Guide to Modeling, Verification, and Applications. Springer, Heidelberg (2003) · Zbl 1024.68072
[9] Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, Springer, Heidelberg (2004) · Zbl 1108.68501 · doi:10.1007/978-3-540-30476-0_19
[10] Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 514–529. Springer, Heidelberg (1996) · doi:10.1007/3-540-61604-7_73
[11] Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer, Three Volumes (1997) · Zbl 0883.68098
[12] Klai, K., Haddad, S., Ilié, J.-M.: Modular verification of Petri nets properties: A structure-based approach. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 189–203. Springer, Heidelberg (2005) · Zbl 1169.68546 · doi:10.1007/11562436_15
[13] Lakos, C., Petrucci, L.: Modular analysis of systems composed of semiautonomous subsystems. In: Int.Conf. on Application of Concurrency to System Design (ACSD), pp. 185–194. IEEE Comp. Soc. Press, Los Alamitos (2004)
[14] Latvala, T., Mäkelä, M.: LTL model-checking for modular Petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 298–311. Springer, Heidelberg (2004) · Zbl 1094.68064 · doi:10.1007/978-3-540-27793-4_17
[15] McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 312–327. Springer, Heidelberg (2000) · Zbl 0974.68520 · doi:10.1007/10722167_25
[16] Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986) · Zbl 0607.68022 · doi:10.1007/BFb0027047
[17] Sibertin-Blanc, C.: A client-server protocol for composition of Petri nets. In: Ajmone Marsan, M. (ed.) Application and Theory of Petri Nets 1993. LNCS, vol. 691, Springer, Heidelberg (1993) · doi:10.1007/3-540-56863-8_57
[18] Souissi, Y., Memmi, G.: Compositions of nets via a communication medium. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 457–470. Springer, Heidelberg (1991) · doi:10.1007/3-540-53863-1_34
[19] Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1(4), 297–322 (1992) · Zbl 0783.68083 · doi:10.1007/BF00709154
[20] Valmari, A.: Composition and abstraction. In: Valmari, A. (ed.) MOVEP. LNCS, vol. 2067, pp. 58–98. Springer, Heidelberg (2000) · Zbl 0985.68036
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.