TOP > 研究報告検索 > ソフトウェアを正しく作る方法と正しさを保証する方法

ソフトウェアを正しく作る方法と正しさを保証する方法

研究報告コード R070000217
整理番号 R070000217
掲載日 2008年4月11日
研究者
  • 青木 利晃
研究者所属機関
報告名称 ソフトウェアを正しく作る方法と正しさを保証する方法
報告概要 現在、ITの進歩により、ソフトウェアの規模、及び、新規ソフトウェアの需要が共に急激に増加し続けています。それらのうち、誤りを含むものは少なくありません。最近でも、航空管制システム、銀行システム、携帯電話などの誤りにより、混乱が引き起こされたことがあります。今後、ますますソフトウェアの規模が大きくなり、社会システムの様々な部分が電子化されていきます。これらのことを考えると、ソフトウェアの正しさを保証する手法の確立が急務です。ソフトウェアの規模が大きくなると、プログラムの直接的な扱いではなく、それを抽象的に記述した分析モデルや設計モデルの重要性が大きくなります。これらのモデルはプログラムを作成する前に作成し、ソフトウェアのアーキテクチャや粒度の大きい単位を記述します。そのため、実装後に誤りが発見されると、コストの高いバックトラックを生じることになってしまいます。幸い、最近では、UML(Unified Modeling Language)など、これらのモデルを詳細に記述するためのダイアグラムが提案されており、それによって記述されたモデルを検証することにより、分析・設計段階で誤りを取り除くことが可能になります。ソフトウェアの検証のためのアプロチーチとしては、定理証明手法とモデル検査手法があります。定理証明手法では、ソフトウェアの性質を推論規則などを用いて対話的に証明することにより、正しさを保証します。モデル検査手法では、ソフトウェアを有限状態で表現し、網羅的に探索して自動的に正しさを保証します。これらの手法には長所と短所があります。前者は、高い記述能力と検証能力を持っていますが、対話的に証明を行うためコストが高くなります。一方、後者は、記述能力が低くソフトウェアを有限状態に抽象化する必要がありますが、自動的に検証を行うことができます。そこで、UMLで記述された分析・設計モデルを、定理証明手法やモデル検査手法を用いて正しさを保証する方法について研究を行っています。さきがけ研究では、定理証明手法の適用に主眼を置いて研究を行いましたが、もう一方のモデル検査手法の適用についても並行して研究を行いました。以下では、定理証明手法による分析・設計モデルの検証法に焦点をあてて説明します。
画像

※ 画像をクリックすると拡大します。

R070000217_01SUM.gif R070000217_02SUM.gif R070000217_03SUM.gif R070000217_04SUM.gif
研究分野
  • 計算機システム開発
関連発表論文 (1) 青木利晃,片山卓也:オブジェクト指向分析モデルの検証支援環境,第19回日本ソフトウェア科学会全国大会論文集(CD-ROM),2002.
(2) 岡崎光隆,青木利晃,片山卓也:並行オブジェクトモデルから並行スレッドモデルヘの変換法,情報処理学会ソフトウェア工学研究会研究報告2003-SE-140,pp.39-46,2003
(3) 立石孝彰,青木利晃,片山卓也:振舞い近似手法を用いたステートチャートに対する不変性の検証,情報処理学会論文誌 Vol.44 No.6,pp. 1448-1460,2003.
(4) 青木利晃,片山卓也:状態遷移図の段階的構築のための論理的碁盤,情報処理学会ソフトウェア工学研究会研究報告2003-SE-143,pp.21-28,2003.
(5) 青木利晃,岸知二,片山卓也:定理証明システムとモデル検査ツールを併用した設計モデルの検証実験,日本ソフトウェア科学会第1回ディペンダブルソフトウェア研究会,pp.49-58,2004.
(6) 青木利晃,片山卓也:オブジェクト指向分析モデルにおけるデータフローの形式化と解析手法,日本ソフトウェア科学会学会誌コンピュータソフトウェア,Vol.21,No.4,pp.1-26,July, 2004.
(7) 青木利晃,岸知二,片山卓也:センサーのモデル化とモデル検査技術の適用について,組込みソフトウェアシンポジウム2004,pp.118-125,2004.
(8) Takaaki Tateishi, Toshiaki Aoki and Takuya Katayama: Successive Behavior Approximation Method for Verifying Distributed Objects, Third International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT'02) , pp.439-446, 2002.
(9) Mitsutaka Okazaki, Toshiaki Aoki and Takuya Katayama: Extracting threads from concurrent objects for the design of embedded systems, Ninth Asia-Pacific Software Engineering Conference 2002, pp.107-116, 2002.
(10) Mitsutaka Okazaki, Toshiaki Aoki and Takuya Katayama: Formalizing sequcnce diagrams and state machines using Concurrent Regular Expression: Proceedings of 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools SCESM'03, pp.74-79, 2003.
(11) Kenro Yatake, Toshiaki Aoki and Takuya Katayama: Collaboration-based Verification of Object-Oriented models in HOL, Proceedings of the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, VVEIS 2004, pp.78-80, 2004.
(12) Toshiaki Aoki and Takuya Katayama: Foundations for Evolutionary Construction of State Transition Models, the Seventh International Workshop on Principles of Software Evolution 2004, pp.143-146, 2004.
研究制度
  • 戦略的創造研究推進事業 さきがけタイプ(旧若手個人研究推進事業を含む)/機能と構成
研究報告資料
  • 青木 利晃. ソフトウェアを正しく作る方法と正しさを保証する方法. 個人型研究(さきがけタイプ)情報・知能分野 研究報告会 先進情報システムとその構成に向けて 「機能と構成」領域 講演要旨集 第Ⅱ期研究者(研究期間2001-2004), 2004. p.7 - 13.

PAGE TOP