Home   >   CSC-OpenAccess Library   >    Manuscript Information
Full Text Available

(255.72KB)
This is an Open Access publication published under CSC-OpenAccess Policy.
Publications from CSC-OpenAccess Library are being accessed from over 74 countries worldwide.
A Tool Generating a C# Code with Contracts of Code Contracts from a VDM++ Model with Conditions
Yuma Yamano, Toshihiko Ando, Keishi Okamoto
Pages - 27 - 39     |    Revised - 30-09-2020     |    Published - 31-10-2020
Volume - 8   Issue - 3    |    Publication Date - October 2020  Table of Contents
MORE INFORMATION
KEYWORDS
Formal Methods, Code Generation, VDM++, C#, Code Contracts.
ABSTRACT
As systems rely on software, the reliability of the software is required. Formal methods are prominent ways to improve the reliability of software. Formal specification is one of the formal methods and offers a formal specification language based on mathematics and computer science. With this method, the ambiguity of the specification can be decreased, and verification can be facilitated. In development based on formal specification, specifications are formally described and then a code is generated from it. This generation is done manually in some cases, but it is done automatically by a tool in some cases. Generally, from the viewpoint of execution efficiency, etc., the generated code is modified, so it is necessary to verify whether the code meets the conditions in the specification. However, this task is manual in many cases, then it is time-consuming and error-prone. In this paper, we introduce a tool to generate a code in the programing language C# from a specification in the formal specification language VDM++. The tool also translates conditions of a specification into contracts of the library Code Contracts of #C. The above problem will be solved with this tool.
1 J. Fitzgerald, P.G. Larsen. Modelling Systems - Practical Tools and Techniques in Software Development. Cambridge: Cambridge University Press, 2009, pp. 1-228.
2 Kyushu University. "FM VDM", Internet: fmvdm.org/, [Aug. 28, 2020].
3 S. Agerholm, P.G. Larsen. "A Lightweight Approach to Formal Methods," in Applied Formal Methods - FM-Trends 98. FM-Trends 1998. Lecture Notes in Computer Science, vol. 1641. 1999, pp. 168-183.
4 T. Kurita, F. Ishikawa and K. Araki. "Practices for Formal Models as Documents: Evolution of VDM Application to Mobile FeliCa IC Chip Firmware," in Formal Methods - 20th International Symposium, 2015, pp. 593-596.
5 P.G. Larsen, K. Lausdahl, N. Battle, J. Fitzgerald, S. Wolff, S. Sahara, M. Verhoef, P.W.V. TranJ�rgensen, T. Oda, P. Chisholm. "VDM-10 Language Manual." Internet: overturetool.org/documentation/manuals.html [Oct. 5, 2020].
6 "Overture Tool." Internet: overturetool.org, [Aug. 28, 2020].
7 J.R. Abrial. Modeling in Event-B: system and software engineering. Cambridge: Cambridge University Press, 2010, pp. 1-586.
8 M. Dalvandi, M. Butler and A. Rezazadeh. "From Event-B Models to Dafny Code Contracts," in 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015), 2015, pp. 308-315.
9 K.R.M. Leino, "Dafny: An automatic program verifier for functional correctness." in Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol. 6355. E.M. Clarke, A. Voronkov, Ed. Berlin, Heidelberg: Springer, 2010, pp. 348-370.
10 V. Rivera, N. Catano, T. Wahls and C. Rueda. "Code generation for Event-B." International Journal on Software Tools for Technology Transfer, vol.19, pp.31-52, Feb. 2017.
11 S. Diswal, P.W.V. Tran-Jørgensen and P.G. Larsen. "Automated Generation of C# and .NET Code Contracts from VDM-SL Models," in THE 14TH OVERTURE WORKSHOP, 2016, pp. 32-47.
12 P.W.V. Tran-Jørgensen, P.G. Larsen and G.T. Leavens. "Automated translation of VDM to JML-annotated Java." International Journal on Software Tools for Technology Transfer, volume 20, pp. 211-235, Apr. 2018.
13 Microsoft. "C# reference." Internet: docs.microsoft.com/en-us/dotnet/csharp/language- reference/, Feb. 14, 2017 [Oct. 5, 2020].
14 Microsoft Research. "Code Contracts." Internet: research.microsoft.com/en- us/projects/contracts/, [Aug. 28, 2020].
15 M. Barnett, K.R.M. Leino and W. Schulte. "The Spec# Programming System: An Overview," in Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2004. Lecture Notes in Computer Science, vol. 3362. G. Barthe, L. Burdy, M. Huisman, JL. Lanet JL and T. Muntean, Ed. Berlin, Heidelberg: Springer, 2005, pp. 49-69.
16 D. Strauss. (2016, Mar. 18). C# Code Contracts Succinctly. [On-line]. Available: www.syncfusion.com/ebooks/csharpcontracts [Oct. 5, 2020].
17 Y. Chisaka and K. Okamoto. "A prototype of a translation tool from VDM++ to C#," in Proceedings of the 78th National Convention of IPSJ. 2016, pp.363-364.
18 D.R. Cok. "OpenJML: JML for Java 7 by Extending OpenJDK," in NASA Formal Methods, Lecture Notes in Computer Science, vol. 6617, pp. 472-479. M. Bobaru, K. Havelund, G.J. Holzmann and R. Joshi, Ed. Berlin Heidelberg: Springer, 2011, pp. 472-479.
19 N. Battle. "VDMJ." Internet: github.com/nickbattle/vdmj, [Aug. 28, 2020].
20 GitHub. "dotnet/Roslyn." Internet: github.com/dotnet/roslyn, [Aug. 28, 2020].
21 Kyushu University. "VDMTools User Manual." Internet: github.com/vdmtools/vdmtools/raw/stable/doc/user-man/usermanpp_a4E.pdf, [Oct. 5, 2020]
22 Galois inc. "SAW - tutorial." Internet: saw.galois.com/tutorial.html, [Aug. 28, 2020].
23 K. Claessen and J. Hughes. "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs," in Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, 2000, pp. 268-279.
Mr. Yuma Yamano
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan
a1811531@sendai-nct.jp
Dr. Toshihiko Ando
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan
Dr. Keishi Okamoto
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan