Abstract
This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: 1) a technique based on simultaneous use of over and under approximations obtained via existential and universal abstractions; 2) a dynamic assume-guarantee reasoning algorithm – previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the ComFoRT model checking tool set and we report encouraging results on an industrial benchmark.
This research was conducted as part of the CMU/SEI IRAD project on Verification of Evolving Software and partially sponsored by the Office of Naval Research (ONR). The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of ONR, the U.S. Government or any other entity.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Alur, R., Cerny, P., Gupta, G., Madhusudan, P., Nam, W., Srivastava, A.: Synthesis of interface specifications for Java classes. In: Symp. on Principles of Programming Languages, POPL (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Chaki, S., Clarke, E., Giannakopoulou, D., Pasareanu, C.S.: Abstraction and assume-guarantee reasoning for automated software verification. Technical Report 05.02, Research Institute for Advanced Computer Science, RIACS (2004)
Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. Formal Methods in System Design 25(2–3) (2004)
Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Chaki, S., Ivers, J., Sharygina, N., Wallnau, K.: The ComFoRT reasoning framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 164–169. Springer, Heidelberg (2005)
Chaki, S., Sharygina, N., Sinha, N.: Verification of evolving software. In: 3rd Workshop on Spec. and Ver. of Component-based Systems, ESEC/FSE (2004)
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzinski, M., Mang, F.Y.C.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 428–441. Springer, Heidelberg (2002)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Alfaro, L.d., Henzinger, T.A.: Interface automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering. ACM Press, New York (2001)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proceedings of the ASE (2002)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 357–370. Springer, Heidelberg (2002)
MAGIC, http://www.cs.cmu.edu/ chaki/magic
McCamant, S., Ernst, M.D.: Early identification of incompatibilities in multi-component upgrades. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 440–464. Springer, Heidelberg (2004)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, pp. 123–144. Springer, New York (1985)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Learning for software, http://www.sei.cmu.edu/staff/chaki/publications/learn-se-trace.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sharygina, N., Chaki, S., Clarke, E., Sinha, N. (2005). Dynamic Component Substitutability Analysis . In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_34
Download citation
DOI: https://doi.org/10.1007/11526841_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)