Search papers, labs, and topics across Lattice.
This paper introduces a novel approach to enhancing the observability of VDM-SL specifications by recording execution traces of assignments, operation calls, and return statements. By utilizing these traces, the authors enable a persistent and analyzable representation of internal operation behaviors, facilitating better validation and debugging processes. The implementation in ViennaTalk and its application to visualization demonstrate significant improvements in understanding and verifying software specifications.
Execution traces can transform VDM-SL specifications into analyzable state-based models, enhancing both validation and debugging capabilities.
VDM has been pursuing rigorous verification through mathematical theorem proving and software testing via simulated execution. Animation through an interpreter enables validation of the specification to ensure it meets the required functionality. Step-by-step execution in a debugger also allows the user to follow the internal behavior of operations. In this paper, we propose the recording and utilization of execution traces of assignments, operation calls, and return statements to make the internal behavior of operations persistent and analyzable as state-based models. The data model of events in execution traces, its implementation in ViennaTalk, and its application to visualization will be introduced.
