Abstract
We present a novel algorithm for interface generation of software components. Given a component, our algorithm uses learning techniques to compute a permissive interface representing legal usage of the component. Unlike our previous work, this algorithm does not require knowledge about the component’s environment. Furthermore, in contrast to other related approaches, our algorithm computes permissive interfaces even in the presence of non-determinism in the component. Our algorithm is implemented in the JavaPathfinder model checking framework for UML statechart components. We have also added support for automated assume-guarantee style compositional verification in JavaPathfinder, using component interfaces. We report on the application of the approach to interface generation for flight-software components.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: Proceedings of POPL 2005, pp. 98–109 (2005)
Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in Model Checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. In: Proceedings of ACM POPL 2002, pp. 4–16 (2002)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Beyer, D., Henzinger, T.A., Singh, V.: Algorithms for Interface Synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 4–19. Springer, Heidelberg (2007)
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)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-Modular Verification for Shared-Memory Programs. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE 2002, pp. 3–12. IEEE Computer Society, Los Alamitos (2002)
Groce, A., Peled, D., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 357. Springer, Heidelberg (2002)
Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive Interfaces. In: Proceedings of ESEC/SIGSOFT FSE 2005, pp. 31–40 (2005)
Java PathFinder, http://javapathfinder.sourceforge.net
Jones, C.B.: Specification and Design of (Parallel) Programs. In: Information Processing 1983: Proceedings of the IFIP 9th World Congress, IFIP, pp. 321–332. North Holland, Amsterdam (1983)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)
Margaria, T., Raffelt, H., Steffen, B., Leucker, M.: The LearnLib in FMICS-jETI. In: Proceedings of ICECCS 2007 (2007)
Mehlitz, P.: Trust Your Model - Verifying Aerospace System Models with Java Pathfinder. In: IEEE/Aero (2008)
Pasareanu, C.S., Giannakopoulou, D., Gheorghiu Bobaru, M., Cobleigh, J.M., Barringer, H.: Learning to Divide-and-Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning. In: FMSD (January 2008)
Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: Logic and Models of Concurrent Systems, vol. 13, pp. 123–144 (1984)
Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: Johansson, T. (ed.) FSE 2003. LNCS, vol. 2887, pp. 188–197. Springer, Heidelberg (2003)
Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: Proceedings of ISSTA 2002, pp. 218–228 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giannakopoulou, D., Păsăreanu, C.S. (2009). Interface Generation and Compositional Verification in JavaPathfinder. In: Chechik, M., Wirsing, M. (eds) Fundamental Approaches to Software Engineering. FASE 2009. Lecture Notes in Computer Science, vol 5503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00593-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-00593-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00592-3
Online ISBN: 978-3-642-00593-0
eBook Packages: Computer ScienceComputer Science (R0)