Automatic Test Data Generation From VDM-SL Specifications

<!DOCTYPE html> <html lang="en" dir="ltr"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <title>Automatic Test Data Generation From VDM-SL Specifications | Richard Atterer</title> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link rel="shortcut icon" href="/sites/all/themes/canvas_spring/favicon.ico" type="image/x-icon" /> <meta name="viewport" content="width=device-width; initial-scale=0.6666; maximum-scale=1.5; minimum-scale=0.25;" /> <link type="text/css" rel="stylesheet" media="all" href="/sites/atterer/files/css/css_20e2e973af54425b6c8758b72a0b4e9d.css" /> </head> <body class="not-front not-logged-in page-node node-type-page no-sidebars"> <div id="page"><div id="page-inner"> <a name="top" id="navigation-top"></a> <div id="skip-to-nav"><a href="#navigation">Skip to Navigation</a></div> <div id="header"><div id="header-inner" class="clear-block"> <div id="header-background"></div> <div id="logo-title"> <div id="logo"><a href="/" title="Home" rel="home"></a></div> </div>  <div id="header-blocks" class="region region-header"> <div id="block-user-0" class="block block-user"> <h2>User login</h2> <div class="content"> <form action="/uni/sep?destination=node%2F40" accept-charset="UTF-8" method="post" id="user-login-form"> <div><div class="form-item" id="edit-name-wrapper"> <label for="edit-name">Username: <span class="form-required" title="This field is required.">*</span></label> <input type="text" maxlength="60" name="name" id="edit-name" size="15" value="" class="form-text required" /> </div> <div class="form-item" id="edit-pass-wrapper"> <label for="edit-pass">Password: <span class="form-required" title="This field is required.">*</span></label> <input type="password" name="pass" id="edit-pass" maxlength="60" size="15" class="form-text required" /> </div> <input type="submit" name="op" id="edit-submit" value="Log in" class="form-submit" /> <div class="item-list"><ul><li class="first last"><a href="/user/password" title="Request new password via e-mail.">Request new password</a></li> </ul></div><input type="hidden" name="form_build_id" id="form-Ug0Ri51eXXOpYXeXNhNQWla3l3i8RiWoj1MvRUNsZrQ" value="form-Ug0Ri51eXXOpYXeXNhNQWla3l3i8RiWoj1MvRUNsZrQ" /> <input type="hidden" name="form_id" id="edit-user-login-block" value="user_login_block" /> </div></form> </div> </div> </div>  </div></div>  <div id="main"><div id="main-inner" class="clear-block with-navbar"> <div id="content"><div id="content-inner"> <div id="content-header"> <div class="breadcrumb"><a href="/">Home</a> › <a href="/research" title="Research">Research</a> › <a href="/uni/sep" class="active">VDM-SL</a></div> <h1 class="title">Automatic Test Data Generation From VDM-SL Specifications</h1> </div>  <div id="content-area"> <div id="node-40" class="node clear-block"> <div class="meta"> <span class="submitted">Last update by Richard on 2010-05-22</span> <div class="terms terms-inline"><ul class="links inline"><li class="taxonomy_term_12 first last"><a href="/uni" rel="tag" title="">uni</a></li> </ul></div> </div> <div class="content"> <div class="sidebar-right"> <div class="toc" id="toc"> <div class="toc-title">Contents</div> <div class="toc-list"> <ol> <li class="toc-level-1"><a href="#what">What is it?</a></li> <li class="toc-level-1"><a href="#purpose">What does it do?</a></li> <li class="toc-level-1"><a href="#formal-methods">About Formal Methods</a></li> <li class="toc-level-1"><a href="#dissertation">Program and Dissertation</a></li> <li class="toc-level-1"><a href="#related">Related Documents</a></li> </ol> </div> </div> </div> <h2 id="what">What is it?</h2> <p>This program and the accompanying dissertation are the result of a software engineering project I did in the 1999/2000 term while studying abroad at the <a href="http://www.cs.qub.ac.uk/">Queen's University of Belfast</a> (Northern Ireland) for one year. The project involved the specification, design, implementation and testing of a program, as well as a presentation of the final result.</p> <h2 id="purpose">What does it do?</h2> <p>The program <code>vdmpart</code> should be regarded as experimental; it is hardly useful without (a lot of) further work. However, it might be of interest to anybody who is acquainted with VDM-SL, the Specification Language of the Vienna Development Model, or is interested in Formal Methods.</p> <p>Below is a short description of the term formal methods, and an explanation of why a tool similar to <code>vdmpart</code> is needed. For a more detailed description of the program, see the introduction and specification sections of the dissertation.</p> <hr/> <h2 id="formal-methods">About Formal Methods</h2> <p>Formal methods are the attempt to avoid some of the problems encountered when developing very large computer programs, such as inappropriate interfaces between components, insufficient documentation from which an implementer cannot tell exactly what behaviour the developer expected, and the difficulty of finding bugs resulting from this. There are two major aspects to formal methods:</p> <ul> <li>Formal specification: The behaviour of each function, class etc. is specified in a quite abstract, mathematical way, mainly using predicate expressions. The languages used for this are very powerful; for example, they support quantifiers. The most popular languages appear to be Z and VDM-SL.</li> <li><p>Verified design: After the abstract specification of the component has been written, it is transformed (possibly with intermediate steps) into a form that more closely resembles a programming language (e.g. not containing any quantifiers). For each such transformation, it is proven that the two ways of describing the behaviour are equivalent.</p> <p>At the end, when the component can be described by something that can be expressed directly in a programming language such as Java, there is a mathematical proof that the code satisfies the abstract specification.</p></li> </ul> <p>Ideally, all the proofs would be performed by a program and the final code would not need any testing since it is known to satisfy the specification. However, in practice there are a number of problems. While the majority of the proofs can be automated, some need human assistance to solve, and that human can make mistakes. Furthermore, it is also possible that the abstract specification contains mistakes which could not be detected automatically. Thus, tests of the final program are as important as with conventionally developed software.</p> <p>Fortunately, when testing software developed with formal methods, one has the advantage that both an abstract specification and an implementation is available. This makes it possible to test for bugs in places where they are most likely, and, very importantly, to automate testing.</p> <p>The basic approach taken by a test data generation tool is to look at the abstract specification, determine values for inputs (e.g. function arguments) and corresponding outputs, and to execute the code with these inputs, comparing the actual and desired outputs. As before, the power of the specification language makes full automation of the test data generation very difficult, if not impossible, but at least for a subset of the language, such a tool can be written.</p> <p><em>If formal methods are so wonderful, why doesn't anybody seem to use them?</em> Formal methods <em>have</em> been used for software with very high quality demands, but indeed, they are not popular at all. The main reasons for this are (in my opinion) the quite significant amount of additional work, and the mathematics involved.</p> <hr/> <h2 id="dissertation">Program and Dissertation</h2> <p>The program is only available as source code - see the end of this page. To compile it, a Unix-like operating system or the CygWin environment under Windows is needed. The source code is distributed under the terms of the GNU GPL.</p> <p>Update: Someone noticed that vdmpart no longer compiles with newer versions of GCC. Below is a patch for GCC 3.3.</p> <h2 id="related">Related Documents</h2> <p>The program is based on the Ph.D. thesis of Christophe Meudec, which is available <a href="http://glasnost.itcarlow.ie/~meudecc/research/thesis/thesis.zip">from his homepage</a> or below.</p> <p>The VDM Specification Language is described in a 1993 ISO draft. That draft has since been superseded, but the final standard is not available for free, so the program is based on the draft.</p> <p>Unfortunately, the draft version seems to have completely dropped off the net around 2002 or so. I am making my local copy available in case someone still has an interest in it.</p> <hr/><div class="field field-type-filefield field-field-file"> <div class="field-label">Attachments: </div> <div class="field-items"> <div class="field-item odd"> <div class="filefield-file"><img class="filefield-icon field-icon-application-pdf" alt="application/pdf icon" src="http://atterer.org/sites/all/modules/filefield/icons/application-pdf.png" /><a href="http://atterer.org/sites/atterer/files/2010-05/vdm-sl/vdmpart-1.0.0.pdf" type="application/pdf; length=389092" title="vdmpart-1.0.0.pdf">My dissertation: Automatic Test Data Generation From VDM-SL Specifications</a></div> </div> <div class="field-item even"> <div class="filefield-file"><img class="filefield-icon field-icon-application-octet-stream" alt="application/octet-stream icon" src="http://atterer.org/sites/all/modules/filefield/icons/application-octet-stream.png" /><a href="http://atterer.org/sites/atterer/files/2010-05/vdm-sl/vdmpart-1.0.0.tar.gz" type="application/octet-stream; length=239340" title="vdmpart-1.0.0.tar.gz">Source code for vdmpart</a></div> </div> <div class="field-item odd"> <div class="filefield-file"><img class="filefield-icon field-icon-text-x-diff" alt="text/x-diff icon" src="http://atterer.org/sites/all/modules/filefield/icons/text-x-generic.png" /><a href="http://atterer.org/sites/atterer/files/2010-05/vdm-sl/vdmpart-1.0.0-040316.diff" type="text/x-diff; length=9389" title="vdmpart-1.0.0-040316.diff">Patch to compile vdmpart with GCC 3.3</a></div> </div> <div class="field-item even"> <div class="filefield-file"><img class="filefield-icon field-icon-application-octet-stream" alt="application/octet-stream icon" src="http://atterer.org/sites/all/modules/filefield/icons/application-octet-stream.png" /><a href="http://atterer.org/sites/atterer/files/2010-05/vdm-sl/meudec-thesis.ps.gz" type="application/octet-stream; length=402826" title="meudec-thesis.ps.gz">Christophe Meudec's thesis: Automatic Generation of Software Test Cases From Formal Specifications</a></div> </div> <div class="field-item odd"> <div class="filefield-file"><img class="filefield-icon field-icon-application-zip" alt="application/zip icon" src="http://atterer.org/sites/all/modules/filefield/icons/package-x-generic.png" /><a href="http://atterer.org/sites/atterer/files/2010-05/vdm-sl/vdmsl_standard.zip" type="application/zip; length=704979" title="vdmsl_standard.zip">VDM-SL draft from 1993</a></div> </div> </div> </div> </div> <ul class="links inline"><li class="comment_add first last"><a href="/comment/reply/40#comment-form" title="Share your thoughts and opinions related to this posting.">Add new comment</a></li> </ul></div> </div> </div></div>  <div id="navbar"><div id="navbar-inner" class="clear-block region region-navbar"> <a name="navigation" id="navigation"></a> <div id="search-box"> <form action="/uni/sep" accept-charset="UTF-8" method="post" id="search-theme-form"> <div><div id="search" class="container-inline"> <div class="form-item" id="edit-search-theme-form-1-wrapper"> <input type="text" maxlength="128" name="search_theme_form" id="edit-search-theme-form-1" size="15" value="Search" title="Enter the terms you wish to search for." class="form-text" /> </div> <input type="hidden" name="form_build_id" id="form-wSbtL48Z4KE-9XGABvXft76F4r0L5I9FIF28npaCMNw" value="form-wSbtL48Z4KE-9XGABvXft76F4r0L5I9FIF28npaCMNw" /> <input type="hidden" name="form_id" id="edit-search-theme-form" value="search_theme_form" /> </div> </div></form> </div>  <div id="primary"> <ul class="links"><li class="menu-344 first"><a href="/photo" title="">Photography</a></li> <li class="menu-362"><a href="/software" title="">Software</a></li> <li class="menu-190"><a href="/jigdo" title="jigdo (Jigsaw Download) - a download manager for CD/DVD images">jigdo</a></li> <li class="menu-376"><a href="/research" title="">Research</a></li> <li class="menu-193 last"><a href="/about" title="About">About</a></li> </ul> </div>  </div></div>  </div></div>  <div id="footer"><div id="footer-inner" class="region region-footer"> <div id="footer-message"><div class="aller"><i>漏 Copyright 2014 Richard Atterer</i></div> <div class="breadcrumb"> <a href="#page"> Top of page </a> • <a href="/"> Home </a> • <a href="/sitemap"> Sitemap </a> • <a href="/contact"> Contact </a> • <a href="/about"> About </a></div></div> </div></div>  </div></div>  <script type="text/javascript" src="/sites/atterer/files/js/js_b0b21dfadec5927599caf5b21dcf2041.js"></script> <script type="text/javascript"> <![CDATA[//><!]]> </script> </body> </html>

CINXE.COM

Automatic Test Data Generation From VDM-SL Specifications | Richard Atterer