Partial order reduction for state/event LTL with application to component-interaction automata. (English) Zbl 1220.68048
Summary: Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.
The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
To bring some evidence of the method’s efficiency, we present some of the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems modelled using the formalism of component-interaction automata.
The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
To bring some evidence of the method’s efficiency, we present some of the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems modelled using the formalism of component-interaction automata.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q45 | Formal languages and automata |
Keywords:
state/event LTL; partial order reduction; formal verification; model checking; component-based systems; component-interaction automataReferences:
| [1] | Chaki, S.; Clarke, E. M.; Ouaknine, J.; Sharygina, N.; Sinha, N.: State/event-based software model checking, Lncs 2999, 128-147 (2004) · Zbl 1196.68129 · doi:10.1007/b96106 |
| [2] | Chaki, S.; Clarke, E.; Ouaknine, J.; Sharygina, N.; Sinha, N.: Concurrent software verification with states, events, and deadlocks, Formal aspects of computing 17, No. 4, 461-483 (2005) · Zbl 1103.68609 · doi:10.1007/s00165-005-0071-z |
| [3] | Brim, L.; Černá, I.; Vařeková, P.; Zimmerova, B.: Component-interaction automata as a verification-oriented component-based system specification, , 31-38 (2005) |
| [4] | Gerth, R.; Peled, D.; Vardi, M. Y.; Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic, , 3-18 (1995) |
| [5] | Zimmerova, B.; Vařeková, P.; Beneš, N.; Černá, I.; Brim, L.; Sochor, J.: The common component modeling example: comparing software component models, Lncs 5153, 146-176 (2008) |
| [6] | N. Beneš, I. Černá, J. Sochor, P. Vařeková, B. Zimmerova, A case study in parallel verification of component-based systems, in: Proceedings of PDMC’08, 2008, pp. 35–51. |
| [7] | Valmari, A.: A stubborn attack on state explosion, Lncs 531, 156-165 (1990) · Zbl 0765.68147 |
| [8] | Peled, D.: All from one, one from all: on model checking using representatives, Lncs 697, 409-423 (1993) |
| [9] | Godefroid, P.: Using partial orders to improve automatic verification methods, Lncs 531, 176-185 (1991) · Zbl 0765.68122 |
| [10] | Peled, D.; Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator, Information processing letters 63, No. 5, 243-246 (1997) · Zbl 1337.68170 |
| [11] | J. Sun, Y. Liu, J.S. Dong, H.H. Wang, Specifying and verifying event-based fairness enhanced systems, in: ICFEM, 2008, pp. 5–24. |
| [12] | Lamport, L.: The temporal logic of actions, ACM transactions on programming languages and systems 16, No. 3, 872-923 (1994) |
| [13] | Bruckner, I.; Wehrheim, H.: Slicing object-Z specifications for verification, Lncs 3455, 414-433 (2005) · Zbl 1118.68541 · doi:10.1007/b135596 |
| [14] | De Alfaro, L.; Henzinger, T. A.: Interface-based design, (2005) |
| [15] | Lynch, N. A.; Tuttle, M. R.: An introduction to input/output automata, CWI quarterly 2, No. 3, 219-246 (1989) · Zbl 0677.68067 |
| [16] | Clarke, E. M.; Grumberg, O.; Peled, D. A.: Model checking, (1999) · Zbl 0847.68063 |
| [17] | Peled, D.: Combining partial order reductions with on-the-fly model-checking, Lncs 818, 377-390 (1994) |
| [18] | Bosnacki, D.; Leue, S.; Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms, Lncs 3925, 271-287 (2006) · Zbl 1178.68336 · doi:10.1007/11691617 |
| [19] | Beneš, N.; Křivánek, M.; Štefaňák, F.: Space effective model checking for component-interaction automata, (2009) · Zbl 1247.68159 |
| [20] | Peled, D.: Ten years of partial order reduction, , 17-28 (1998) |
| [21] | Holzmann, G. J.; Peled, D.: An improvement in formal verification, , 197-211 (1994) |
| [22] | The CoIn Team, CoIn tool–formal verification tool for component interaction automata. URL: http://anna.fi.muni.cz/coin/tool/. |
| [23] | N. Beneš, L. Brim, I. Černá, J. Sochor, P. Vařeková, B. Zimmerova, The CoIn tool: modelling and verification of interactions in component-based systems, in: Proceedings of the Workshop on Formal Aspects of Component Software, FACS’08, 2008, pp. 221–225. |
| [24] | Giannakopoulou, D.; Magee, J.: Fluent model checking for event-based systems, , 257-266 (2003) |
| [25] | Barnat, J.; Brim, L.; Ročkai, P.: Divine 2.0: high-performance model checking, , 31-32 (2009) |
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.
