×

SAT-based verification for timed component connectors. (English) Zbl 1279.68212

Summary: Component-based software construction relies on suitable models underlying components, and in particular the coordinators which orchestrate component behaviour. Verifying correctness and safety of such systems amounts to model checking the underlying system model. The model checking techniques not only need to be correct (since system sizes increase), but also scalable and efficient.
In this paper, we present a SAT-based approach for bounded model checking of timed constraint automata, which permits true concurrency in the timed orchestration of components. We present an embedding of bounded model checking into propositional logic with linear arithmetic. We define a product that is linear in the size of the system, and in this way overcome the state explosion problem to deal with larger systems. To further improve model checking performance, we show how to embed our approach into an extension of counterexample guided abstraction refinement with Craig interpolants.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q45 Formal languages and automata
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

FOCI; Esterel; Chaff; Reo
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, Rajeev: Timed automata, Lncs 1633, 8-22 (1999) · Zbl 1046.68574
[2] Arbab, Farhad: What do you mean, coordination?, Bulletin of the Dutch association for theoretical computer science (NVTI), 11-22 (1998)
[3] Arbab, Farhad: Reo: a channel-based coordination model for component composition, Mathematical structures in computer science 14, No. 3, 329-366 (2004) · Zbl 1085.68552
[4] Arbab, Farhad; Baier, Christel; De Boer, Frank S.; Rutten, J. J. M.M.: Models and temporal logical specifications for timed component connectors, Software and system modeling 6, No. 1, 59-82 (2007)
[5] Arbab, Farhad; Baier, Christel; Rutten, J. J. M.M.; Sirjani, M.: Modeling component connectors in reo by constraint automata (extended abstract), Electronic notes in theoretical computer science 97, 25-46 (2004) · Zbl 1105.68058
[6] Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.: Bounded model checking for timed systems, Lncs 2529, 243-259 (2002) · Zbl 1037.68549
[7] Baeten, J. C. M.: A brief history of process algebra, Theoretical computer science 335, No. 2–3, 131-146 (2005) · Zbl 1080.68072
[8] Baeten, J. C. M.; Middelburg, C. A.: Process algebra with timing, (2002) · Zbl 1021.68063
[9] Berry, Gérard: The foundations of esterel, Proof, language, and interaction, 425-454 (2000)
[10] Biere, Armin; Cimatti, Alessandro; Clarke, Edmund M.; Strichman, Ofer; Zhu, Yunshan: Bounded model checking, Advances in computers 58, 118-149 (2003)
[11] Bonsangue, M. M.; Clarke, D.; Silva, A.: Automata for context-dependent connectors, Lncs 5521, 184-203 (2009)
[12] Cardelli, Luca: Real time agents, Lecture notes in computer science 140, 94-106 (1982) · Zbl 0493.68017
[13] Clarke, E. M.; Biere, A.; Raimi, R.; Zhu, Y.: Bounded model checking using satisfiability solving, Formal methods in system design 19, No. 1, 7-34 (2001) · Zbl 0985.68038
[14] Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM 50, No. 5, 752-794 (2003) · Zbl 0974.68517
[15] David Costa, Formal Models for Component Connectors, Ph.D. Thesis, Vrije Universiteit Amsterdam, 2010.
[17] Fokkink, Wan: Introduction to process algebra, (2000) · Zbl 0941.68087
[18] Hähnle, R.: Short CNF in finitely-valued logics, Lncs 689, 49-58 (1993)
[19] Henzinger, T. A.; Jhala, R.; Majumdar, R.; Mcmillan, K. L.: Abstractions from proofs, Popl, 232-244 (2004) · Zbl 1325.68147
[20] Jhala, R.; Mcmillan, K. L.: Interpolant-based transition relation approximation, Lncs 3576, 39-51 (2005) · Zbl 1081.68622
[21] Kemper, Stephanie: SAT-based verification for timed component connectors, Electronic notes in theoretical computer science 255, 103-118 (2009) · Zbl 1366.68172
[22] Kemper, Stephanie; Platzer, A.: SAT-based abstraction refinement for real-time systems, Electronic notes in theoretical computer science 182, 107-122 (2007)
[23] Larsen, Kim Guldstrand; Milner, Robin: Verifying a protocol using relativized bisimulation, Lecture notes in computer science 267, 126-135 (1987) · Zbl 0628.68022
[25] Mcmillan, K. L.: An interpolating theorem prover, Lncs 2988, 16-30 (2004) · Zbl 1126.68573
[26] Milner, R.: Communication and concurrency, (1989) · Zbl 0683.68008
[27] Milner, Robin: Calculi for synchrony and asynchrony, Theoretical computer science 25, 267-310 (1983) · Zbl 0512.68026
[28] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S.: Chaff: engineering an efficient SAT solver, , 530-535 (2001)
[29] Pratt, Vaughan R.: Modeling concurrency with geometry, , 311-322 (1991)
[30] Reed, G. M.; Roscoe, A. W.: A timed model for communicating sequential processes, Theoretical computer science 58, 249-261 (1988) · Zbl 0655.68031
[31] Tripakis, Stavros: Verifying progress in timed systems, Lecture notes in computer science 1601, 299-314 (1999)
[32] Yi, W.: CCS + time = an interleaving model for real time systems, Lncs 510, 217-228 (1991) · Zbl 0769.68027
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.