一般的に，ソフトウェアのライフサイクルには2つの検証工程がある．1つはシステムの機能的な仕様が記述されたモデルの検証であり，もう1つはそのシステムの実際に動作するCなどのようなプログラミング言語により記述されたコード（ソースコード）の試験である．我々は，この両方の工程で利用可能な検証器を開発した．モデル検証は，質の高い試験を行う助けとなる．すでにいくつかの検証ツールが存在するが，それらはモデルかソースコードかのいずれかを対象としている．我々のツールはその両方を検証，試験することが可能である．ソースコードを検証するときには，GDB上で試験対象となるコードを実行し，そのコードに対応するモデルの構成要素を除いたモデルの一部と同期させて試験する．モデルは，我々のツールではプロセス代数に基づいた言語により記述される．ソースコードの状態空間は削除された構成要素と他の要素の間の通信に利用されるアクションに対応したソースコード上のブレイクポイントの集合として定義される．このツールでは最初の検証工程で作成されたシステムのモデルをソースコードの試験に再利用することが可能である．本稿では，簡単な例としてECHOサービスを示す．In general, there are two checking processes within the lifecycle of a system. One is verification of models describing functional specification, and the other is testing of real codes implementing the system. We developed a model checking tool can being used on both processes. Model checking systematically explores the state space of systems. The systems are expressed as the model or real code (or source code) written in programming languages such as C. There are several model checking tools that handle either the models or the real codes, but not both. In testing processes of the real codes, our model checking tool checks both the models and the real codes.The tool executes the binary code on GDB, then examines a composition with the model from which the portions of the model that correspond to the code being executed have been eliminated. A state space of the real code is a set of GDB's breakpoints corresponding to actions to communicate between the eliminated portion and others, so the model is written in a modeling language based on process algebra. This tool enables the re-use of the same model that was used in verification processes. We will illustrate ECHO service as a simple example.
各種検索
サポート
ヘルプ