Abstract
The problem of formal software specification has been addressed and discussed since the infancy of software engineering. However, among all the proposed solutions, none is universally accepted yet. Many different formal descriptions can in fact be given for the same software component; thus, the problem of determining the consistency relation among those descriptions becomes relevant and potentially critical. In this work, we propose a method for comparing two specific kinds of formal specifications of containers. In particular, we check the consistency of intensional behavior models with algebraic specifications. The consistency check is performed by generating a behavioral equivalence model from the intensional model, converting the algebraic axioms into temporal logic formulae, and then checking them against the model by using the NuSMV model checker. An automated software tool which encodes the problem as model checking has been implemented to check the consistency of recovered specifications of relevant Java classes.
This research has been partially funded by the European Commission, Programme IDEAS-ERC, Project 227977-SMScom.
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
Guttag, J.V., Liskov, B.: Program Development in Java: Abstraction, Specification and Object-Oriented Design. Addison-Wesley, Reading (2001)
Ghezzi, C., Jazayeri, M., Mandrioli, D.: Fundamentals of Software Engineering. Prentice Hall PTR, Upper Saddle River (2002)
Harel, D., Gery, E.: Executable object modeling with statecharts. In: ICSE 1996: 18th International Conference on Software Engineering (1996)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10(1) (1978)
Ernst, M.D.: Dynamically Discovering Likely Program Invariants. Ph.D. thesis, University of Washington, Seattle, Washington (August 2000)
Ghezzi, C., Mocci, A., Monga, M.: Synthesizing intensional behavior models by graph transformation. In: ICSE 2009: Proc. of 31st Int. Conf. on Soft. Eng. (2009)
Henkel, J., Reichenbach, C., Diwan, A.: Discovering documentation for Java container classes. IEEE Trans. Software Eng. 33(8), 526–543 (2007)
Baresi, L., Ghezzi, C., Mocci, A., Monga, M.: Using graph transformation systems to specify and verify data abstractions. In: Proc. of GT-VMT 2008 (2008)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Mosses, P.D. (ed.): CASL Reference Manual. LNCS (IFIP Series), vol. 2960. Springer, Heidelberg (2004)
Doong, R., Frankl, P.G.: The ASTOOT approach to testing object-oriented programs. ACM Trans. on Soft. Eng. and Meth. 3(2) (1994)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs in TCS. Springer, Heidelberg (2005)
Spy Checker Website (2009), http://home.dei.polimi.it/mocci/spy/check/
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Tr. Softw. Eng. Methodol. 12(4) (2003)
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Uchitel, S., Chatley, R., Kramer, J., Magee, J.: Goal and scenario validation: a fluent combination. Requir. Eng. 11(2), 123–137 (2006)
Ivkovic, I., Kontogiannis, K.: Tracing evolution changes of software artifacts through model synchronization. In: ICSM 2004. IEEE Computer Society, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghezzi, C., Mocci, A., Salvaneschi, G. (2010). Automatic Cross Validation of Multiple Specifications: A Case Study. In: Rosenblum, D.S., Taentzer, G. (eds) Fundamental Approaches to Software Engineering. FASE 2010. Lecture Notes in Computer Science, vol 6013. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12029-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-12029-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12028-2
Online ISBN: 978-3-642-12029-9
eBook Packages: Computer ScienceComputer Science (R0)