Model checking is a fundamental technique for verifying finite state concurrent systems. Traditionally, model designs were initially created to facilitate the application of model checking. This process, representative of Model Driven Development (MDD), involves generating an equivalent code from a given model which is verified before implementation begins. However, this approach is considerably slower compared to agile development methods and lacks flexibility in terms of expandability and refactoring. We have proposed "CodoMo: Python Code to Model Generator for pyModelChecking." This tool automates the transformation of a Python code by an AST static analyzer and a concolic testing tool into intermediate models suitable for verification with pyModelChecking, bridging the gap between traditional model checking and agile methodologies. Additionally, we have implemented a multiprocess approach that integrates the execution of PyExZ3 with the generation of Kripke structures achieving greater work efficiency. By employing CodoMo, we successfully verified a Tello Drone programming with gesture-based image processing interfaces, showcasing the tool's powerful capability to enhance verification processes while maintaining the agility required for today's fast-paced development cycles.

翻译：模型检测是验证有限状态并发系统的基础技术。传统上，模型设计最初是为了便于应用模型检测而创建的。这一过程作为模型驱动开发（MDD）的代表，涉及从已验证的给定模型生成等效代码，然后才开始实施。然而，与敏捷开发方法相比，这种方法速度明显较慢，且在可扩展性和重构方面缺乏灵活性。我们提出了“CodoMo：面向pyModelChecking的Python代码到模型生成器”。该工具通过AST静态分析器和混合执行测试工具，将Python代码自动转换为适合使用pyModelChecking进行验证的中间模型，从而弥合了传统模型检测与敏捷方法之间的差距。此外，我们实现了一种多进程方法，将PyExZ3的执行与Kripke结构的生成相结合，从而实现了更高的工作效率。通过使用CodoMo，我们成功验证了基于手势图像处理接口的Tello无人机编程，展示了该工具在保持当今快节奏开发周期所需敏捷性的同时，增强验证流程的强大能力。