使用ProB对Prolog转换系统进行动画制作、验证和可视化
Animation, Verification and Visualisation of Prolog Transition Systems with ProB
浏览论文内容
中文总结 AI 辅助
介绍了基于Prolog的ProB工具，阐述其Prolog动画模式的现有功能及扩展，如统计检查模拟、可靠跟踪重放等，通过四子棋等案例研究展示新功能用途，对Event-B证明及教学演示模型等应用有帮助。
中文摘要 AI 辅助
ProB是用于高级形式规范的基于Prolog的模型检查器、动画制作工具和约束求解器。人们还可以用ProB为Prolog谓词定义的转换系统制作动画，以应用其各种验证技术。本文介绍了ProB的Prolog动画模式的现有功能及其近期扩展。扩展功能包括用于统计检查的模拟、更可靠的跟踪重放、带用户输入的转换以及改进的状态可视化。我们将这些新功能应用于案例研究，特别是评估游戏玩法中的不同策略，如四子棋。这些功能对许多其他应用也很有用，尤其是对ProB用于Event-B证明义务的新相继式证明器，以及与交互式可视化结合用于教学的演示模型。
英文摘要
ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB's new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.
发表机构
- Faculty of Mathematics
- Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universit\" a tsstr. 1, D-40225 D\" u sseldorf
机构由 AI 辅助整理，请以论文原文为准。
