形式手法 (MALACS)

研究内容概要

MALACS (Models And Languages for Correct Software)グループは,ソフトウェア開発に関連した形式手法技術を研究しています.モデル検査,定理証明,形式的仕様記述などが含まれます.

モデル検査では,システムの状態をモデル化し不都合な状態遷移の発生を見つけることで,モデルの正しさを客観的に示します.正しいモデルに従ってソフトウェア開発を行うことで,開発の手戻りを軽減することができます.

形式手法の中でヘビーウェイトと言われている定理証明は,モデル検査などで避けられない状態爆発の問題が発生しないため注目を集めています.ソフトウェアの挙動を関数として定義し,その関数が満すべき性質を証明することで挙動の正しさを保証します.証明が与えられた関数から実際に動作するプログラムコードを生成し,プログラム開発時のバグ発生を抑制することができます.

形式的仕様記述手法は,曖昧さのない言語でソフトウェアなどの仕様を正確に表現するための一連の手法を指します.そのような手法を用いて仕様を記述することにより,仕様の曖昧さを解消し,仕様内の抜け漏れや誤りなどを表面化させることができます.そのため,これらは,システムに対する正確な理解,複数人の間での理解の共有,早期の分析・検証を促進する手法であると言えます.

研究トピックの紹介

Java Pathfinderなどを使ったソフトウェアモデル検査

Java PathFinder (JPF) は,NASA を中心に開発されているJavaプログラムのオープンソースソフトウェアモデル検査器である.この研究テーマでは,複数プログラムがネットワーク通信を行 うシステムのモデル検査を,JPFを用いて行う手法の開発に取り組んでいる.

ソフトウェアモデル検査器は,本来的に1つのプロセスのみを対象とするものである.通信する複数のプロセスのうちの1つだけをモデル検査の対象とす ると,バックトラックの際に他のプロセスとの通信の同期が取れないという問題がある.我々はこの問題の解決法として「I/O キャッシュ層」を提案している.通信の実行を監視する層を設け,バックトラックを行うモデル検査対象とその他のプロセスとの整合をとるものである.我々は これを実現するモジュールを開発・保守しており,現在ではJPFと共に配布されている.

2011年度以降は,この基礎技術を,クラウドコンピューティング環境の基盤ソフトウェアの検証に応用する計画である.この仕事は,山本(千葉大),Artho (産総研),萩谷(東大),Platonとの共同研究として実施されている.

様相mu計算の多値意味論

数理的技法の応用として,近年では,ソースコードを直接検証する手法が広く研究されている.これを可能にする技術のひとつが抽象化である.プログラ ムの実行状態全体は巨大な集合になり,直接解析することは困難である.適切な抽象化によって,多数の類似した実行状態(具体状態) を1つの抽象状態にまとめることができれば,解析が可能となる.我々は,リスト,木,DAG などのポインタで構成されたデータ構造を扱うプログラム(以下,ポインタ操作プログラムと呼ぶ) に関する検証のために,様相論理の一種である,拡張様相μ計算と呼ばれる一群の論理を用いて抽象化を行う手法を提案している.

現在は,停止性の検証を行うためN∞値クリプキ構造を利用するアプローチを試みている.N∞は,自然数の集合に最大元∞ を添加したものである.適切な代数構造を導入することで,論理式の「真偽値」をN∞の要素で与えることができる.完全な真・偽はそれぞれ0 と∞ であり,他の値はその中間となる.ポインタ操作プログラムの停止問題はN∞値クリプキ構造における充足可能性判定問題に帰着させることができるので,この 判定法およびその前提としてのモデル検査法の解明を目指している.

探索を通した形式仕様の部分的・段階的な活用の支援

最近,形式仕様の技術に対し,国内産業界での注目が非常に高まっている. 一方,厳密な仕様を十分に記述することに対して, 工数の懸念や難しさの問題がある. また,仕様モデルに時間をかける代表的な手法の印象から, 本質的・潜在的には有用な原則や技術があるはずであっても, アジャイル開発や品質保証テストのコミュニティーには 「関係ない」と思われがちな技術でもある.

これに対し本研究では,プログラムの動作実装前のスケルトンを出発点とし, 形式仕様の技術を部分的,段階的に活用するツールを提供することを目指している. 提案ツールの入力は,Javaプログラムのスケルトンに対し, 仕様やテスト方針の記述を付与したものである. ただし,この記述は,場合分けや一例の指定など, 断片的であってもよく,またスケルトンそのものだけでもよい. その入力に対し,提案ツールは制約ソルバーなどを用い, その記述から想定される様々なテストケース例を探索,提示する.

このツールは,具体例を提示させ人手で確認していくような, 現状の手作業を少し強化するような利用もできる. 一方,具体例を踏まえて制約などを繰り返し追記していけば, 段階的に十分な形式仕様を構築するような利用もできる. 以上により,形式化や自動化を, 必要最小限に活用できるようにすることを目指している. また,テスト駆動開発,形式仕様構築,テスト設計といった 作業対象に共通して活用できるものとする.

形式的仕様の段階的詳細化における抽象度の系統的な制御

ソフトウェア開発の初期段階で系統的な分析を行う必要性が叫ばれている。形式仕様記述手法はそのような分析に効果的であると言われる。 中でも段階的詳細化による形式仕様記述は、先に厳密かつ抽象的な仕様を記述し、後で記述したより具体的な仕様との整合性を証明することを繰り返すことで厳密な仕様を段階的に構築するというアプローチであり、ソフトウェアの複雑さに対処しつつ厳密な分析を可能にする。 このアプローチは、段階的詳細化を主眼に置いた手法Event-Bが学術界と産業界の両方で活発に研究されるなど、近年注目を集めている。

形式仕様が作られる前には通常自然言語で記述された非形式的文書が作られる。 段階的詳細化による厳密な仕様記述を行うためには、非形式的文書に記述されているソフトウェアの要素や振舞いや性質のうちどれをどの抽象度の仕様に反映するかを決定する詳細化の計画をする必要がある。 この際、厳密性のために詳細化の整合性を保証するルールに従うように詳細化を行う必要がある一方、複雑さに対処するために仕様記述者が容易に仕様を把握できるような詳細化を行うことが望ましい。 しかし、詳細化を多段階にし過ぎてルールに違反したり、逆にルールに従うと把握の難しい仕様を記述してしまうなどすることが多く、厳密性と複雑さへの対処の両立のためには記述の際に多くの試行錯誤が必要である。 それにも関わらず、詳細化の計画については既存の研究ではごく限られた領域の仕様の記述に対する指針が示されている程度であり、一般的でかつ系統的な詳細化計画に関する研究はなされていない。

望ましい詳細化の計画のために判断する必要のある事項は多岐に渡り、それが計画の難しさの原因となっているが、それらの事項は「本質的に仕様記述者が判断する必要のある部分」と「手法のルールなどから機械的に判断できる部分」に分けられると考えられる。 そこで本研究ではこれらを分離し、後者の判断のために必要な事項を入力として受け取り後者に関連する試行錯誤を自動的に行う機構を提供する。 さらに、入力を作成する指針を提供することにより機構の適用を促進する。

具体的には、非形式的文書の要素のうちどれが反映されるかを系統的に扱うために、本研究で非形式的文書の要素として、システムの状態遷移の制約を表す「性質」とシステムの構成要素や振舞いを表す「事象」の2種類を考え、性質に対応する記述が形式仕様に導入される順序を詳細化計画と定義する。 その上で、望ましい詳細化のための7つのゴールを提案し、それらの優先順位を考慮して対話的に詳細化計画の探索を行う手法を提案した。この手法について、段階的詳細化による形式仕様記述手法として代表的なEvent-Bを対象とし、Event-Bの作者による例題を題材に実験を行い、Event-Bの作者による計画と手法の出力を比較したところ、いずれの例でも作者による計画と同等の計画を含む出力が得られた。

メンバー

  • 田辺 良則(特任教授)
  • 石川 冬樹(准教授)
  • 小林 努(D3)
  • Fernando Tarin(D3)

連絡先

小林 努:

研究成果

主な発表文献

  1. 前岡 淳,田辺 良則,石川 冬樹,Java PathFinder における探索打ち切りポリシーを用いたヒューリスティック探索,日本ソフトウェア科学会 コンピュータソフトウェア Vol.30, No.3 「ソフトウェア工学」特集,2013年8月
  2. Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden, Systematic Planning of Refinement in Event-B, The 4th Rodin User and Developer Workshop at iFM 2013, June 2013 (to appear)
  3. Tsutomu Kobayashi and Shinichi Honiden: Towards Refinement Strategy Planning for Event-B, Workshop on the experience of and advances in developing dependable systems in Event-B (DS-Event-B'12) in conjunction with ICFEM, November 2012
  4. Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya: Modal μ-calculus on min-plus algebra N-infinity, コンピュータソフトウェア (採録決定)
  5. Fuyuki Ishikawa, Toward Customizable and Bi-directionally Traceable Transformation between VDM++ and Java, The 9th Overture/VDM Workshop at FM 2011, June 2011
  6. 石川 冬樹,山本 佳代子,本位田 真一,物理的相互作用に着目した,スマート空間の形式仕様記述と検証,情報処理学会論文誌Vol.52 No.1,pp.220-232,2011年1月
  7. 田辺良則, Cyrille Artho, 萩谷 昌己, Watcharin Leungwattanakit, 山本 光晴: ネットワークアプリケーションのマスタースレーブ方式によるソフトウェアモデル検査. 第8回ディペンダブルシステムワークショップ (DSW2010summer), 2010.07.20
  8. 姜 帆,田辺 良則,本位田 真一,Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出,第14回プログラミングおよびプログラミング言語ワークショップ
  9. 姜 帆, Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出, 第7回 TPPミーティング
  10. 日野 克重, 本位田 真一, ソフトウェアの問題記述のための実行可能な形式化自然語の提案, 情報処理学会論文誌Vol.52, No.3, pp.1-30, 2011年3月.
  11. Alexis Goyet, Masami Hagiya and Yoshinori Tanabe: Decidability and undecidability results on the modal mu-calculus with a natural number-valued semantics, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Lecture Notes in Artificial Intelligence, Vol.6188, 2010, pp.148-160.
  12. Yoshinori Tanabe and Masami Hagiya: Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus. 6th Workshop on Fixed Points in Computer Science (FICS 2009), Coimbra, Portugal, 12-13 September 2009, pp. 108--115.
  13. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto: Cache-Based Model Checking of Networked Applications: From Linear to Branching Time. ASE 2009: 447-458
  14. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe: Efficient Model Checking of Networked Applications. TOOLS (46) 2008: 22-40