Abstract
Testing and verification are two activities which have the same objective: to ensure software dependability. In the Java context, the Java Modelling Language (JML) has been proposed as specification language. It can be used both for verification and test. Usually, the JML specification is designed with a specific purpose: test or verification. This article addresses the question of reusability of a JML specification provided for one activity (resp. verification or test) in the other context (resp. test or verification). Two different case studies are considered.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. 4, 32–54 (2005)
Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M., Requet, A.: JACK—a tool for validation of security and behaviour of Java applications. In: 5th International Symposium Formal Methods for Components and Objects (FMCO). Lecture Notes in Computer Science, vol. 4709, pp. 152–174. Amsterdam, The Netherlands (2006)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: the KeY Approach. Springer, New York (2007)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS’03). Electronic Notes in Theoretical Computer Science, vol. 80, pp. 73–89 (2003)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. STTT 7, 212–232 (2005)
Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: The 12th International FME Symposium, Pisa, Italy (2003)
Chalin, P.: Early detection of JML specification errors using ESC/Java2. In: Proceedings of the 2006 Conference on Specification and Verification of Component-Based Systems (SAVCBS), pp. 25–32. Portland, Oregon (2006)
Cheon, Y., Leavens, G.T.: A runtime assertion checker for the java modeling language (JML). In: Arabnia, H.R., Mun, Y. (eds.) International Conference on Software Engineering Research and Practice (SERP ’02), pp. 322–328. Las Vegas, Nevada (2002)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: the JML and JUnit way. In: 16th European Conference on Object-Oriented Programming (ECOOP’02), pp. 231–255 (2002)
du Bousquet, L., Ledru, Y., Maury, O., Oriat, C., Lanet, J.-L.: A case study in JML-based software validation (short paper). In: Automated Software Engineering (ASE). Linz, Austria (2004)
du Bousquet, L., Nakamura, M., Yan, B., Igaki, H.: Using formal methods to increase confidence in one home network system implementation. Case study. In: Workshop on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2007). Revue des Nouvelles Technologies de l’Information, vol. RNTI-SM-1. Poitiers, France (2007)
Filliâtre, J.-C., Marché, C.: The why/krakatoa/caduceus platform for deductive program verification. In: 19th International Conference Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 173–177. Berlin, Germany (2007)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234–245 (2002)
JML: The java modeling language (JML) home page (2008). http://www.cs.iastate.edu/~leavens/JML.html
JUnit: JUnit (2008). http://www.junit.org
Leavens, G., Baker, A., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)
Ledru, Y., Dadeau, F., du Bousquet, L., Ville, S., Rose, E.: Mastering combinatorial explosion with the tobias-2 test generator. In: 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), pp. 535–536. USA (2007)
Ledru, Y., du Bousquet, L., Maury, O., Bontron, P.: Filtering TOBIAS combinatorial test suites. In: Fundamental Approaches to Software Engineering (FASE’04). LNCS, vol. 2984. Barcelona, Spain (2004)
Loke, S.W.: Service-oriented device ecology workflows. In: First International Conference on Service-Oriented Computing (ICSOC 2003). Lecture Notes in Computer Science, vol. 2910, pp. 559–574. Trento, Italy (2003)
Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. J. Log. Algebr. Program. 58(1–2), 89–106 (2004)
Maury, O., Ledru, Y., du bousquet, L.: Using TOBIAS for the automatic generation of VDM test cases. In: Third VDM Workshop (in conjunction with FME’02) (2002)
Nakamura, M., Tanaka, A., Igaki, H., Tamada, H., Matsumoto, K.: Adapting legacy home appliances and web services. In: Int. Conf. on Web Services (ICWS 2006), pp. 849–858 (2006)
Nakamura, M., Tanaka, A., Igaki, H., Tamada, H., Matsumoto, K.: Constructing home network systems and integrated service using legacy home appliances and web services. Int. J. Web Serv. Res. 5(1) (2009)
Oriat, C.: Jartege: a tool for random generation of unit test for java classes. In: First International Conference on the Quality of Software Architechtures and Second International Workshop of Software Quality (QoSa/SOQUA). Lecture Notes in Computer Science, vol. 3712, pp. 242–256 (2005)
Papazoglou, M.P., Georgakopoulos, D.: Special issue: service-oriented computing. Introduction. Commun. ACM 46(10), 24–28 (2003)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
du Bousquet, L., Ledru, Y., Maury, O. et al. Reusing a JML Specification Dedicated to Verification for Testing, and Vice-Versa: Case Studies. J Autom Reasoning 45, 415–435 (2010). https://doi.org/10.1007/s10817-009-9132-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9132-y