Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2018

11.02.2017 | Regular Paper

Automated translation of VDM to JML-annotated Java

verfasst von: Peter W. V. Tran-Jørgensen, Peter Gorm Larsen, Gary T. Leavens

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-based elements such as invariants and pre- and postconditions into account during the code-generation process. The contract-based elements of the Vienna Development Method Specification Language (VDM-SL) are translated into corresponding constructs in the Java Modelling Language (JML) and used to validate the generated code against the properties of the VDM model. VDM-SL and JML are both Design-by-Contract (DbC) languages, with the difference that VDM-SL supports abstract modelling and system specification, while JML is used for detailed specification of Java classes and interfaces. We describe the semantic differences between the contract-based elements of VDM-SL and JML and formulate the translation as a set of rules. We further demonstrate how dynamic JML assertion checks can be used to ensure the consistency of VDM’s subtypes when a model is code-generated. The translator is fully automated and produces JML-annotated Java programs that can be checked for correctness using JML tools.
Vorheriger Artikel PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
With the recent introduction of pure operations into VDM-10 (not to be confused with pure methods in JML), it has become possible to invoke operations, albeit pure ones, from a function. This feature was introduced to address issues with the object-oriented dialect of VDM, called VDM++, but was made available in every VDM-10 dialect (including VDM-SL).
 
2
The generated code uses variables to represent the patterns (record pattern, tuple pattern, identifier pattern, etc.) introduced by use of pattern matching in VDM.
 
Literatur
1.
Meyer, B.: Object-Oriented Software Construction. Prentice-Hall International, Upper Saddle River (1988)
2.
Bjørner, D., Jones, C. (eds.): The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol. 61. Springer (1978)
3.
4.
Fitzgerald, J.S., Larsen, P.G., Verhoef, M.: Vienna Development Method. Wiley Encyclopedia of Computer Science and Engineering. Wiley (2008)
5.
Woodcock, J., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Hertfordshire, UK (1996)
6.
Jones, C.B.: Software Development A Rigorous Approach. Prentice-Hall International, Englewood Cliffs (1980)MATH
7.
8.
Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7, 212–232 (2005)CrossRef
9.
Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010). doi:10.​1145/​1668862.​1668864 CrossRef
10.
11.
Jørgensen, P.W.V., Couto, L.D., Larsen, M.: A code generation platform for VDM. In: Proceedings of the 12th Overture workshop (2014)
12.
Cok, D.: OpenJML: JML for Java 7 by Extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 6617, pp. 472–479. Springer, Berlin. doi:10.​1007/​978-3-642-20398-5_​35(2011)
13.
Larsen, P.G., Lausdahl, K., Battle, N., Fitzgerald, J., Wolff, S., Sahara, S., Verhoef, M., Tran-Jørgensen, P.W.V., Oda, T., Chisholm, P.: The VDM-10 Language Manual. Tech. Rep. TR-2010-06, The Overture Open Source Initiative (2010)
14.
Andrews, D., Bruun, H., Damm, F., Dawes, J., Hansen, B., Larsen, P., Parkin, G., Plat, N., Totenel, H.: A Formal Definition of VDM-SL. Tech. Rep. 1998/9, Leicester University (1998)
15.
Lausdahl, K., Larsen, P.G., Battle, N.: A deterministic interpreter simulating a distributed real time system using VDM. In: Qin, S., Qiu, Z. (eds.) Proceedings of the 13th International Conference on Formal methods and Software Engineering. Lecture Notes in Computer Science, vol. 6991, pp. 179–194. Springer, Berlin. doi:10.​1007/​978-3-642-24559-6_​14. ISBN 978-3-642-24558-9 (2011)
16.
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual, revision 2344 edn. (2013)
17.
18.
19.
20.
Yi, J., Robby, Deng, X., Roychoudhury, A.: Past expression: encapsulating pre-states at post-conditions by means of AOP. In: Proceedings of the 12th Annual International Conference on Aspect-oriented Software Development, AOSD ’13, pp. 133–144. ACM. doi:10.​1145/​2451436.​2451453 (2013)
21.
McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Western Joint Computer Conference (1961)
22.
Tran-Jørgensen, P.W.V.: Automated translation of VDM-SL to JML-annotated Java. Department of Engineering, Aarhus University, Tech. rep. (2016)
23.
Larsen, P.G., Lausdahl, K., Battle, N.: Combinatorial testing for VDM. In: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM ’10, pp. 278–285. IEEE Computer Society, Washington, DC, USA. doi:10.​1109/​SEFM.​2010.​32. ISBN 978-0-7695-4153-2 (2010)
24.
Tran-Jørgensen, P.W.V., Larsen, P.G., Battle, N.: Using JML-based code generation to enhance test automation for VDM models. In: Proceedings of the 14th Overture Workshop (2016)
25.
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-Oriented Systems. Springer, New York (2005). doi:10.​1007/​b138800 MATH
26.
Vilhena, C.: Connecting between VDM++ and JML. Master’s thesis, Minho University with exchange to Engineering College of Aarhus (2008)
27.
Jin, D., Yang, Z.: Strategies of modeling from VDM-SL to JML. In: International Conference on Advanced Language Processing and Web Information Technology, pp. 320–323 (2008)
28.
Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, Boston (2004)
29.
Zhou, J., Jin, D.: Research on modeling from VDM-SL to JML for systematic software development. Control and Decision Conference (CCDC). 2010 Chinese, pp. 2312–2317. IEEE, Xuzhou (2010)
30.
Larsen, P.G.: Ten years of historical development: “Bootstrapping” VDMTools. J. Univers. Comput. Sci. 7(8), 692–709 (2001)MATH
31.
Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for event-B. Int. J. Softw. Tools Technol. Transf. 19:1–22 (2015)
32.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
33.
Lensink, L., Smetsers, S., van Eekelen, M.: Generating verifiable Java code from verified PVS specifications. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 310–325. Springer, Berlin. doi:10.​1007/​978-3-642-28891-3_​30 (2012)
34.
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer, Saratoga (1992)
35.
36.
Hubbers, E., Oostdijk, M.: Generating JML specifications from UML state diagrams. In: Forum on Specification and Design Languages FDL’03, Frankfurt, Germany, pp 263–273, September 23–26, 2003
37.
Zhen, Z.: Java Card Technology for Smart Cards. Prentice-Hall, Boston (2000)
38.
Klebanov, A.: Automata-based programming technology extension for generation of JML annotated Java card code. In: Proceedings of the Spring/Summer Young Researchers’ Colloquium on Software Engineering, pp. 41–44 (2008)
39.
Cok, D.R.: Reasoning with specifications containing method calls and model fields. J. Object Technol. 4(8), 77–103 (2005)CrossRef
Metadaten
Titel
Automated translation of VDM to JML-annotated Java
verfasst von
Peter W. V. Tran-Jørgensen
Peter Gorm Larsen
Gary T. Leavens
Publikationsdatum
11.02.2017
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-017-0448-3

Weitere Artikel der Ausgabe 2/2018

International Journal on Software Tools for Technology Transfer 2/2018 Zur Ausgabe

TACAS 2016

Coqoon

TACAS 2016

The Tinker tool for graphical tactic development

TACAS 2016

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata

TACAS 2016

Multi-core symbolic bisimulation minimisation

Introduction

Recent advances in interactive and automated analysis

TACAS 2016

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives