Home本研究成果のポイント
〇テストに基づいた形式検証（TBFV: Testing-Based Formal Verification）の適用可能性を広げるため、Java パッケージが適用する機能検証に対する公理的な手法を提案
〇よく利用される Vector、 ArrayList、 LinkedList クラスが提供する主要な機能の意味を形式的に定義するための公理を確立
〇事例と実験により TBFV の有効性と限界を議論
概 要
ソフトウェアテストはプログラムのバグを検出することができるがバグがないことを保証することはできない。一方、述語論理と形式的意味論に基づいた演繹的形式検証はプログラムの正確性を保証することができるが実際のプログラムに適用するには多くの課題がある。このように相反する性質を持つソフトウェアテストと形式検証を組み合わせて、互いの利点の活用し欠点を回避するプログラム検証手法を開発することは非常に挑戦的な課題である。
我々の先行研究では、テストに基づいた形式検証（TBFV: Testing-Based Formal Verification）を提案し、形式的な仕様に基づいたソフトウェアテストと演繹的形式検証で使われる Hoare 理論を融合することで、プログラムの実行パスに関する正確性を検証する方法を議論した。TBFV は、形式的な仕様で定義された機能シナリオからテストケースを自動的に生成し、テストケースの実行パスから正しさを示す定理を形成する。最終的に、その定理を証明することで機能シナリオが正しく実装されることを保証する。この新しい手法は実用的なソフトウェア検証において非常に有望であるが、まだいくつかの課題が残っている。重要な課題の一つとして、パッケージで定義された機能をどのようにして扱うかが挙げられる。
本研究では、TBFVの適用可能性を拡張するため、上記の問題に関して公理的なアプローチを提案した。特に、Java の標準パッケージで提供される Vector、 ArrayList、 LinkedList クラスに焦点を当て、これらのクラスが提供する主要な機能の正確性を定義する一連の公理を示した。また、公理を形式検証に利用する例を示し、実験を通じて、それらの有効性と限界を分析した。さらに研究では、TBFV についてのいくつかの課題も明らかになった。理論的には、事後条件から定義された公理を利用した自動的な実行パスの事前条件の導出を通じて、形成された定理の検証まで自動的に実行できる。しかしながら完全な自動化を行うためには、プログラムのシグネチャー（変数名など）を保持しておく必要がある。これはプログラムを実装する側で対処する必要があるため、必ずしも完全な自動化が実行できない場合がある。もう一つの課題は、ツールの不足であり、より大規模なプログラムに適用するための効率的なツールの開発が必要となる。
【論文情報】
A. Liu and S. Liu, "Enhancing the Capability of Testing-Based Formal Verification by Handling Operations in Software Packages," in IEEE Transactions on Software Engineering, vol. 49, no. 1, pp. 304-324, 1 Jan. 2023, doi: 10.1109/TSE.2022.3150333.
