GDBとシステムモデルを用いたソースコード検証器の開発

• Item type: Trans(1)
• 公開日: 2006-07-15
• タイトル: GDBとシステムモデルを用いたソースコード検証器の開発
• タイトル / 言語: en
• タイトル: Direct Model Checking of Real Codes Using GDB and System Models
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 東京工業大学大学院情報理工学研究科計算工学専攻，有限会社プレシステム
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology , PRESYSTEMS, Inc.
• 著者名: 永藤, 直行
• 著者名(英): Naoyuki, Nagatou
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 一般的に，ソフトウェアのライフサイクルには2つの検証工程がある．1つはシステムの機能的な仕様が記述されたモデルの検証であり，もう1つはそのシステムの実際に動作するCなどのようなプログラミング言語により記述されたコード（ソースコード）の試験である．我々は，この両方の工程で利用可能な検証器を開発した．モデル検証は，質の高い試験を行う助けとなる．すでにいくつかの検証ツールが存在するが，それらはモデルかソースコードかのいずれかを対象としている．我々のツールはその両方を検証，試験することが可能である．ソースコードを検証するときには，GDB上で試験対象となるコードを実行し，そのコードに対応するモデルの構成要素を除いたモデルの一部と同期させて試験する．モデルは，我々のツールではプロセス代数に基づいた言語により記述される．ソースコードの状態空間は削除された構成要素と他の要素の間の通信に利用されるアクションに対応したソースコード上のブレイクポイントの集合として定義される．このツールでは最初の検証工程で作成されたシステムのモデルをソースコードの試験に再利用することが可能である．本稿では，簡単な例としてECHOサービスを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 47, 号 SIG11(PRO30), p. 1-12, 発行日 2006-07-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会