| ||||
| ||||
![]() Title:Enhancing Testing of VDM-SL models Conference:Overture 16 Tags:code-generation, continuous validation, unit testing and VDM Abstract: Testing of VDM-SL models is currently a tedious and error-prone task due to lack of support for defining tests, executing tests automatically, and validating test results. In VDM++, test-driven development is supported by the VDMUnit framework, which offers many of the features one would expect from a modern testing framework. However, since VDMUnit relies on object-orientation and exception handling, this framework does not work for testing VDM-SL models. In this paper, we discuss the challenges of testing VDM-SL models, and propose a library extension of Overture/VDMUnit that improves this situation. We demonstrate usage of this library extension, and show how it also enables one to reuse tests to validate code-generated VDM-SL models. Enhancing Testing of VDM-SL models ![]() Enhancing Testing of VDM-SL models | ||||
Copyright © 2002 – 2025 EasyChair |