Abstract
The challenge of model checking of isolated software components becomes more and more relevant with the boom of component-oriented technologies [20]. An important issue here is how to verify an open model representing an isolated software component (also referred as the missing environment problem in [7]).
In this paper, we propose on-the-fly simulation of the component environment to address the issue. We employ behavior protocols [18] and a system coordinating two model checkers: Java PathFinder [4] and BPChecker [15]. This approach allows us to enclose the model representing the behavior of a given component and consequently to exhaustively verify the model. Our solution was implemented as the Carmen tool [1].
We demonstrate scalability of our approach on real-life examples and show that, in comparison with the COMBAT model checker [17], we bring better performance, and also exhaustive and correct verification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Carmen Project (2008), http://www.lifl.fr/~plsek/projects/carmen/
CoCoMe Project (2008), http://agrausch.informatik.uni-kl.de/CoCoME
Fractal Project (2008), http://fractal.ow2.org/
Java PathFinder Model Checker (2008), http://javapathfinder.sourceforge.net/
SOFA Project (2008), http://sofa.objectweb.org/
Adamek, J., Bures, T., Jezek, P., Kofron, J., Mencl, V., Parizek, P., Plasil, F.: Component Reliability Extensions for Fractal Component Model (2008), http://kraken.cs.cas.cz/ft/public/public_index.phtml
Bergstra, J.A., Ponse, A., Smolka, S.A.: Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Bulej, L., Bures, T., Coupaye, T., Decky, M., Jezek, P., Parizek, P., Plasil, F., Poch, T., Rivierre, N., Sery, O., Tuma, P.: CoCoME in Fractal. In: Proceedings of the CoCoME project (June 2007)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Laubach, R.S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. of the 22nd International Conference on Software Engineering (June 2000)
Engler, D., Dunbar, D.: Under-constrained Execution: Making Automatic Code Destruction Easy and Scalable. In: International Symposium on Software Testing and Analysis (ISSTA) (2007)
Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. Int. Journal on Software Tools for Technology Transfer (STTT) 6(4)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Component Verification with Automatically Generated Assumptions. Journal of Automated Software Engineering 12(3) (July 2005)
Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619. Springer, Heidelberg (2003)
Mach, M., Plasil, F., Kofron, J.: Behavior Protocol Verification: Fighting State Explosion. Published in the Int. Journal of Computer and Inf. Science 6(1), 22–30 (2005)
Parizek, P., Plasil, F.: Specification and Generation of Environment for Model Checking of Software components. In: Proc. of Formal Foundations of Embedded Software and Component-Based Software Architectures, vol. 176(2) (May 2007)
Parizek, P., Plasil, F., Kofron, J.: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker. In: Proceedings of 30th IEEE/ NASA Software Engineering Workshop (SEW-30) (January 2007)
Plasil, F., Visnovsky, S.: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering 28(11) (November 2002)
Plsek, A.: Extending Java PathFinder with Behavior Protocols. Master Thesis (2006), http://www.lifl.fr/~plsek/projects/carmen/download/documents/masterThesis.pdf
Szyperski, C.: Component Software: Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley Professional, Boston (2002)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering Journal 10(2) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Plšek, A., Adámek, J. (2008). Carmen: Software Component Model Checker. In: Becker, S., Plasil, F., Reussner, R. (eds) Quality of Software Architectures. Models and Architectures. QoSA 2008. Lecture Notes in Computer Science, vol 5281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87879-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-87879-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87878-0
Online ISBN: 978-3-540-87879-7
eBook Packages: Computer ScienceComputer Science (R0)