CodoMo: Python Model Checking to Integrate Agile Verification Process of Computer Vision Systems

TL;DR

CodoMo addresses the challenge of integrating formal verification with agile computer vision development by semi-automating the extraction of intermediate models from Python code using an AST-based state extractor and PyExZ3 concolic testing, then feeding these models into pyModelChecking for verification. The approach leverages a multiprocessing pipeline to parallelize state extraction and model generation, resulting in Kripke structures that can be checked against CTL*/LTL properties, demonstrated on a gesture-controlled Tello drone with 224 sample images. Key contributions include the State Extractor and Model Generator components, a data-driven modeling strategy, and evidence that agile verification can be applied to real-world CV systems, albeit with limitations such as state-space explosion and the need for additional tooling for on-the-fly checking. Overall, CodoMo shows promise for bringing formal verification closer to modern agile development in CV applications, with potential extensions to internal drone metrics and alternative Python-based model checkers.

Abstract

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.

Figures (7)

• Figure 1: CodoMo system architecture
• Figure 2: A snippet of an original code
• Figure 4: On-the-fly multiprocessing architecture of the concolic testing process and the model generation process
• Figure 5: Experimental setup for drone gesture control
• Figure 6: Skeleton extraction process for hand gesture recognition