Title of article :
SAT-based verification for timed component connectors
Author/Authors :
Mark S. Kemper، نويسنده ,
Issue Information :
دوهفته نامه با شماره پیاپی سال 2012
Pages :
20
From page :
779
To page :
798
Abstract :
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.
Keywords :
Timed constraint automata , Abstraction refinement , model checking , SAT , Component-based software engineering
Journal title :
Science of Computer Programming
Serial Year :
2012
Journal title :
Science of Computer Programming
Record number :
1080279
Link To Document :
بازگشت