The Community for Technology Leaders
2012 35th Annual IEEE Software Engineering Workshop (2006)
Columbia, Maryland
Apr. 24, 2006 to Apr. 28, 2006
ISSN: 1550-6215
ISBN: 0-7695-2624-1
pp: 133-141
Pavel Parizek , Charles University, Czech Republic
Frantisek Plasil , Charles University, Czech Republic; Academy of Sciences of the Czech Republic
Jan Kofron , Charles University, Czech Republic; Academy of Sciences of the Czech Republic
ABSTRACT
Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols [1], which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking.
INDEX TERMS
software components, behavior protocols, model checking, cooperation of model checkers
CITATION
Pavel Parizek, Frantisek Plasil, Jan Kofron, "Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker", 2012 35th Annual IEEE Software Engineering Workshop, vol. 00, no. , pp. 133-141, 2006, doi:10.1109/SEW.2006.23
80 ms
(Ver 3.3 (11022016))