CodoMo：Python 模型检查以集成计算机视觉系统的敏捷验证流程
软件工程
2024-12-12 v1
摘要
模型检查是验证有限状态并发系统的基础技术。传统上，模型设计最初是为了便于应用模型检查而创建的。该过程代表了模型驱动开发（MDD），涉及从给定模型生成等效代码，在实现开始前进行验证。然而，该方法与敏捷开发方法相比速度慢得多，且在可扩展性和重构方面缺乏灵活性。我们提出了"CodoMo：Python 代码到模型生成器，用于 pyModelChecking。"该工具通过 AST 静态分析器和符号执行测试工具将 Python 代码自动转换为适合用 pyModelChecking 进行验证的中间模型，弥合了传统模型检查与敏捷方法之间的差距。此外，我们实现了一种多进程方法，将 PyExZ3 的执行与克里普克结构的生成相集成，从而提高了工作效率。通过使用 CodoMo，我们成功验证了一个基于手势的图像处理接口的 Tello 无人机编程，展示了该工具在保持当今快速开发周期所需的敏捷性的同时增强验证过程的强大能力。
引用
@article{arxiv.2412.08159,
title = {CodoMo: Python Model Checking to Integrate Agile Verification Process of Computer Vision Systems},
author = {Yojiro Harie and Yuto Ogata and Gautam Bishnu Prasad and Katsumi Wasaki},
journal= {arXiv preprint arXiv:2412.08159},
year = {2024}
}
备注
Article accepted/presented as Long Paper at The Twelfth International Symposium on Computing and Networking (CANDAR2024)