Download Tutorial for Overture/VDM-SL

Tutorial to Overture/VDM-RT
Figure 3.7: Creating a New VDM-SL Project
Figure 3.8: The VDM-SL Standard Libraries
3.5
Debugging
This section describes facilities for debugging a model by stepping through the evaluation of functions and operations. The alarm example is used. The following test file (testalarm.vdmsl)
can be found in the alarm project and it is provided in Appendix A.2.
By using the values defined in this test file, it is possible to exercise the system in order to
check whether, for this test, the correct expert is paged as a result of a given alarm.
3.5.1
The Debug configuration
Before the debugging can be initiated in Overture, a debug configuration must be created by rightclicking the project and choosing Debug As → Debug configuration.
8