高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software
１．研究目的
数学に基づき開発されたソフトウェアの要求定義と機能検証を厳密的に行うことができる従来の形式手法（例えば、VDM[1]、B-Method[2]、CafeOBJ[3]など）の使い難い点と間違いやすい点を改善し、効率的な形式仕様作成技術およびソフトウェア欠陥の自動検出技術を提案することが、本研究の目的である。具体的に

劉 少英 (Shaoying LIU, Ph. D.)

は、様々な機能を明確に定義する形式仕様を表すテン法政大学 情報科学部 教授

プレートである仕様パターンを用いて、ソフトウェア(Professor, Hosei University, Faculty of Computer andInformation Sciences)

機能の形式仕様を効率的に作成する技術、考え漏れたIEEE Computer Society British Computer Society 日本ソフトウェア

機能や安全性の制約を発見するために仕様の整合性と科学会

妥当性を厳密的に検査する手法と支援ツールおよび形受賞：国際会議 ICECCS’ 96 優秀論文賞 (1996) Fellowship of British式仕様に基づくプログラムの自動テスト技術の開発をComputer Society (2010)目指す。

著書：Formal Engineering for Industrial Software Development Using
the SOFL Method, Springer-Verlag, 2004
研究専門分野：ソフトウェア工学

２．研究背景集合論、論理学、代数などを含む離散数学に基づき開発された形式手法は、ソフトウェアの信頼性を向上させる最も厳密的なモデル駆動（model-driven）開発技術と考えられる。その中核となる形式仕様記述技術
は、高信頼性と安全性が求められるシステム開発企業で採用されたこともある。しかし、形式仕様記述プロ

はじめに情報通信ソフトウェアシステムに潜む欠セスの中でどのような側面を考慮すれば、考え漏れた

陥は、信頼性・安全性の問題を引き起し、延いてはシ機能や安全性の制約を発見でき、埋め込まれた欠陥をステムトラブル、ダウンによる莫大なエネルギー損失自動的に検出できるかということには、課題がまだ残と、大きな環境問題、社会問題と発展しかねない。特っている。更に、企業の開発現場で形式手法の使い難にインターネット、スマートフォンなど急増する情報い点と間違いやすい点もあることが判明し、形式手法通信システムに使われる基盤ソフトウェア、OS およが企業で普及することはなかなか困難な局面になってび様々な応用ソフトウェア（オンライン銀行システム、いる。

航空券予約購入システムなど）には高い信頼性・安全

このような課題を解決するために、形式仕様パター性の確保が必要であり、開発期間とコストを大幅に減ン、形式仕様の検証および形式仕様に基づくプログラ

らすことは情報通信ソフトウェア産業にとって喫緊のムの自動テストに関して、様々な研究が行われた。

重要課題であり、依然として解決していない。

Stepney et al.は、形式仕様を作成するに使われる 6 種

そこで、本研究では、効率的な形式仕様記述技術お類の仕様パターンを提案し、小さな事例で仕様パターよび形式仕様に基づく自動テスト技術の研究を行った。

ン の 役 割 を 説 明 し た [4] 。 同 じ よ う な 考 え で 、前者では、ソフトウェアシステムへの要求と設計に関Ackermann と Turowski は 、 Unified Modelling

する考え漏れた機能および安全性に関わる欠陥を防ぐLanguage（UML）に使われている形式仕様記述言語ことができ、後者では、開発されたプログラムに埋めOCL に対して、様々な仕様パターンを提案した[5]。

込まれた欠陥を効率的に検出することができる。

また、Leveson グループは、SpecTRM-RL という要求

1

TELECOM FRONTIER No.91 2016 SPRING

高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software
仕様記述言語で形式仕様を記述することを支援するツ

関しては、Parnas グループはカナダの Darlington 原ール SpecTRM を研究開発した[6]。

子発電所用ソフトウェアの検証するプロジェクトを通ソフトウェア要件定義或いは設計の形式仕様の検証

じ、Document Driven Inspection（DDI）という形式に関しては、Heyer が UML で作成した機能要求を表仕様に基づくプログラム検査手法を提案した [9]。

すユースケース図に含まれている操作に対して、事前Khurshid グループは、形式仕様言語 Alloy で記述し条件と事後条件を作成した上でシステム設計を反映すた操作仕様の事前条件によってテストケースの自動生るシーケンス図の妥当性を検査する手法を提案した

成技術を提案し、この技術の支援ツール TestEra を研[7]。ここで、事前条件とは、操作の入力が満たすべき究開発した [10]。

条件であり、事後条件とは、操作の出力が満たさなければならない条件である。Heitmeyer グループは、

３．研究方法Software Cost Reduction（SCR）という表式言語で記実用性が高い形式仕様記述言語 SOFL（Structured

述される形式仕様の整合性を自動的に検査する技術をObject-Oriented Formal Language）を基に、図 1 に提案した[8]。

示すソフトウェア開発プロセスと支援技術を研究開発

形式仕様に基づくプログラム検査とテストの研究にした。

システムの非形式要求
１．機能
２．データリソース
３．安全性、効率、品質等 の制約検証された形式仕様

要求と設計の形式化をしながら漏れた機能と他の欠陥の自動検出モジュール System;
データ定義
プロセス A1
事前条件1
事後条件1
end_process;
プロセス A2
事前条件2
事後条件2
end_process;

A2
A1

A4
A3

プロセス A3
事前条件3
事後条件4
end_process;end_module;

プログラムの作成

プログラム

プログラムの欠陥の自動検出検出された欠陥
１．欠陥１
２．欠陥２...
n. 欠陥ｎ

図１ SOFL でのソフトウェア開発プロセス

2

TELECOM FRONTIER No.91 2016 SPRING

高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software
最初に、自然言語でシステムの機能、データリソー従来の方法で記述することが必要である。このようにスおよび安全性等の制約を含む非形式要求仕様を簡潔作成される SOFL 形式仕様の構造は、図 1 の中で右側に作成する。次に、実用性が高い SOFL 形式仕様記述の部分に示されている。

言語で、その非形式仕様に基づき形式仕様を記述しな形式仕様の整合性と妥当性を保証するために、形式がら、システムの様々な機能、データ構造および制約仕様のアニメーションによる厳密な検査技術を開発しを細かく検討する。この過程を効率的に行うために、た[12]-[16]。形式仕様の中でシステムの構造を表す条仕様パターンに基づく形式仕様を作成する手法を提案

件データフロー図（CDFD）に基づき、形式仕様に定した[11]。一つの仕様パターンには、パターン名、パ義された機能シナリオを自動的に導出して、それぞれターンを使える条件、パターンの要素および形式表現の機能シナリオで表す振る舞いのアニメーションを行のテンプレートが含まれている。仕様パターンが効率いながら、その機能シナリオの整合性と妥当性を検査的に検索したり適用したりするために、全ての仕様パする。一つの機能シナリオは、入力データフローからターンは木構造にまとめられる。コンピュータがこの出力データフローまでの操作シーケンスである。機能ような木構造を利用して、形式仕様を作成する開発者

シナリオのアニメーションとは、そのシナリオに含まと交信しながら、機能要求の形式仕様を作成することれている操作の振る舞いを入力データと出力データ間ができる。また、この過程の中で、開発者は支援ツーの関係を視覚的に表現することである。このようなアルからのガイドを受け取りながら、機能と安全性の制ニメーションによって、形式仕様の整合性を検査する

約を完全に理解することができ、事前に考えられなかことができ、妥当性を確認することもできる。全てのった機能と制約を引き出し、漏れた機能と制約を自動重要な性質を確認した上で、形式仕様によってプログ的に検出することも可能である。但し、現在の技術でラムを作成する。この仕様検査技術の支援ツールのスは、一つのプロセス（操作）の事前条件と事後条件をナップショットを図 2 に示す。

形式的に表現することができるが、仕様の他の部分を

図２ 形式仕様のアニメーションによる検査技術の支援ツール

3

TELECOM FRONTIER No.91 2016 SPRING

高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software
図の左上部分は、条件データフロー図 CDFD およびテスト条件の原子論理式により、入力変数に代入する

それにより抜き出された機能シナリオの一部を示す。

テストケースとした値を生成する。生成されたテスト

図の右部分は、厳密な検査を行うためにツールとユーケースは、必ずその原子論理式を満たす。次は、原子ザの交信状況を示す。図の左下部分は、選択された機論理式から構成された論理積という論理式を満たす入能シナリオのアニメーションを行うために必要なテス力変数のテストケースを生成する。このため、原子論トケースの生成に関するエリアである。

理式間の入力変数の依存関係によって、論理積に含ま作成されたプログラムに含まれる欠陥を効率的に検れる全ての原子論理式を原子論理式集合に分ける。こ出するために、形式仕様に基づくプログラムテスト技

れらの集合を用いて、適切なアルゴリズムによって、術を提案した[17],[18]。図 3 に示すように、この技術テストケースを自動的に生成する。最後に、論理和にでテストを行うためには、三つの段階が必要である。

よって、テスト条件を満たすテストケースの集合を生第一段階で、形式仕様を基にテストケースを自動的に成する。また、テスト結果を分析するために、欠陥が生成する。第二段階で、生成されたテストケースを用プログラムに存在するかどうかを判定できるテストオいてプログラムを実行させる。第三段階で、実行したラクルを明確に定義し、それを形式仕様から自動的に結果を分析する。

抜き出すアルゴリズムも確立した。これらの技術を支

本研究では、テストケースの生成を効率的に行うた援するソフトウェアツールのプロトタイプも開発した。

めに、操作の機能を定義した形式仕様の事前条件と事

但し、本自動テスト技術では、欠陥がどのプログラム後条件を生かして、テストケースを自動的に生成するパスに含まれるかまでは確定できるが、そのパスの中方法とアルゴリズムを開発した。具体的には、事前条で具体的な場所およびその欠陥の種類を確定すること件と事後条件によってテストケースを生成するためにはできない。更に、テスト対象としたプログラムを実必要な「テスト条件」を自動的に形成して、それに基行させる「ドライブモジュール」の自動生成アルゴリづいてテストケースを自動的に生成する。テスト条件

ズムは、自動テスト技術の実現にとって不可欠であるとは、事前条件と事後条件にあるガード条件の論理積が、それはまだ開発していない。

であり、その中に操作の出力変数が含まれていない。

テストケースの自動生成

操作の形式仕様：
process A(入力変数）出力変数
事前条件
事後条件
end_process

プログラムの実行
プログラム：
A(入力変数）出力変数｛
Javaプログラミング言語で作成されたアルゴリズム}
テスト結果の分析

図３ 形式仕様に基づくテスト技術の基本原理

4

TELECOM FRONTIER No.91 2016 SPRING

高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software[3] K. Futatsugi and A. Nakagawa. An Overview of

４．将来展望CAFE Specification Environment: an Algebraic

本研究で提案したソフトウェア開発における欠陥防止と欠陥検出の自動化技術は、高信頼情報通信ソフト

ApproachforCreating,Verifying,andウェアを含む幅広い応用領域のソフトウェア開発に適Maintaining

FormalSpecifications

over用できるが、完全に自動化を実現するには課題が残っNetworks.

Proceedingsている。主な課題は、ソフトウェアの要求仕様の品質Internationalを保証するために、仕様の完全性と様々な一致性といEngineering

う性質を仕様から自動的に抜き出すアルゴリズムの確

Computer Society Press, pp. 170-181. 1997.

立と、それらの性質を自動的にテストする技術の開発[4] S. Stepney, F. Polack, and I. Toyn. An Outline

および効率的な支援ツールの開発にある。また、上述

Pattern Language for Z: Five Illustrations andした形式仕様に基づくプログラムテストに関する課題

Two Tables. ZB 2003, LNCS 2651, Springer, pp.

も残っている。

2-19. 2003.

ofConference
Methods

theFirst

onFormal(ICFEM’97),

IEEE

これらの課題を系統的に解決するためには、論理式[5] J. Ackermann and K. Turowski. A Library ofによるテストケースの自動生成技術と定理証明理論おOCL Specification Patterns for Behavioral

よびプログラムの正確性を証明する Hoare 論理と適Specification of Software Components. 18th

切に統合して、形式仕様の様々な性質を自動的に検証Internationalでき、プログラムの欠陥の自動検出技術を開発するこInformation Systems Engineering (CAiSE'06),とが重要である。具体的には、「自動テストに基づく形

Springer-Verlag, pp. 255-269. 2006.

ConferenceonAdvanced

式検証」という新たな理論と方法および支援ツールの[6] N. G. Leveson, J. D. Reese, and M. P. E.

開発に集中することである。潜在的な課題としては、

Heimdahl. SpecTRM: A CAD System for Digital

どのようにして自動テストを定理証明プロセスに統合

Automation.

して、実用性と有効性と共に高い形式検証方法を確立

Avionics System Conference (DASC 98), The

し、また、どのようにして十分なテストケースを効率

AIAA/IEEE/SAE, vol. 1, pp. B52/1-B52/8. 2003.

的かつ自動的に生成できるかということである。この[7] T. Heyer. Semantic Inspection of Early UML

Proceedings

IEEEofTransactions

17th

ような課題を解決して確立する形式検証技術では、ソDesigns.

on

フトウェア仕様の様々な性質を表す定理の有効性の判

Engineering, 28(4), pp. 413-430. 2002.

DigitalSoftware定ができ、プログラムに含まれる欠陥をより効率的に[8] C. L. Heitmeyer and R. D. Jeffords and B. G.

検出することができる。これによって、ソフトウェア

Labaw. Automated Consistency Checking ofの生産性を向上させることができるだけではなく、ソ

Requirements Specifications. ACM Transactions

フトウェア構築プロセスの中でエラー防止や開発され

on Software Engineering and Methodology, 5(3),たソフトウェアの信頼性、安全性および堅牢性を向上

pp. 231-261. 1996.
[9] D. L. Parnas and J. Madey and M. Iglewski.

させることもできる。

PreciseDocumentationof

Well-StructuredPrograms. IEEE Transactions on SoftwareEngineering, 20(12), pp. 948-976. 1994.

参考文献[1] C. B. Jones. Systematic Software Development[10]S.

KhurshidandD.

Marinov.

TestEra:Using VDM. 2nd edition, Prentice Hall. 1990.

Specification-based Testing of Java Programs[2] J. R. Abrial. The B-Book: Assigning Programs tousing SAT. Journal of Automated Software

Meanings. Cambridge University Press. 1996.

Engineering, 11(4), pp. 403-434. 2004.

5TELECOM FRONTIER No.91 2016 SPRING

高信頼情報通信ソフトウェア開発における欠陥防止と検出の自動化に関する研究
Research on Automatic Techniques for Prevention and Detection of Defects in Development ofDependable Information Communication Software[11] X. Wang and S. Liu. An Approach to Declaring
Data Types for Formal Specifications. 3rdInternational Workshop on SOFL + MSVL
(SOFL+MSVL 2013), LNCS 8332, Springer, pp.
135-153. 2013.
[12] M. Li and S. Liu. Automated Functional
Scenarios-based

FormalAnimation.

Asia-Pacific

19th

Specification
SoftwareEngineering Conference (APSEC 2012), pp.
107-115. 2012.
[13]M.

LiandS.

Liu.

Reviewing

FormalSpecification for Validation Using Animation
andTraceLinks.

Proceedingsof21thAsia-Pacific Software Engineering Conference(APSEC 2014), pp.286-293. 2014.
[14] M. Li and S. Liu. Traceability-Based Formal
Specification Inspection. Proceedings of EighthInternational Conference on Software Security
and Reliability (SERE), pp.167-176. 2014.
[15] S. Liu, F. B. Zainuddin, and M. Li. Integrating
Animation into Informal Specification Writing
for Requirements Analysis. Proceedings of 3rdInternational

Conference

onInformatics

Engineering and Information Science (ICIEIS2014), SDIWC, pp. 136-143. 2014.
[16] M. Li and S. Liu. Tool Support for Rigorous
Formal Specification Inspection. Proceedings ofIEEE

17thInternational

ConferenceonComputational Science and Engineering (CSE2014), pp.729-734. 2014.
[17] S. Liu. Utilizing Hoare Logic to Strengthen
Testing for Error Detection in Programs. The
Turing Centenary Conference, Manchester, UK,
EPiC Series, pp. 229-238. 2012.
[18]S.

LiuandS.

Nakajima.

Combining

Specification-Based Testing, Correctness Proof,
and Inspection for Program Verification inPractice.

Proceedingsof3rdInternational

この研究は、平成２３年度ＳＣＡＴ研究助成の対象とWorkshop on SOFL+MSVL (SOFL+MSVL 2013),して採用され、平成２４～２６年度に実施されたもの

LNCS 8332, Springer, pp. 3-16. 2013.

です。
6TELECOM FRONTIER No.91 2016 SPRING