AI 中文总结
本文针对VDM-SL规格，提出记录并利用执行跟踪以持久化、分析操作内部行为的方法，介绍相关数据模型、ViennaTalk实现及可视化应用。
AI 中文摘要
VDM（维也纳开发方法）一直通过数学定理证明追求严格验证，并通过模拟执行开展软件测试。解释器驱动的动画可验证规格是否符合所需功能，调试器中的分步执行也能让用户跟踪操作的内部行为。本文提出记录并利用赋值、操作调用及返回语句的执行跟踪，使操作的内部行为持久化并可作为基于状态的模型分析，将介绍执行跟踪中事件的数据模型、其在ViennaTalk中的实现及其在可视化中的应用。
英文摘要
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.
Commentsthe 24th Overture Workshop
