形式的仕様とプログラムの厳密なレビューの自動化についての研究

• 研究課題/領域番号: 14019081
• 研究種目: 特定領域研究
• 配分区分: 補助金
• 審査区分: 理工系
• 研究機関: 法政大学
• 研究代表者: 劉 少英 法政大学, 情報科学部, 教授 (90264960)
• 研究期間 (年度): 2002
• 研究課題ステータス: 完了 (2002年度)
• 配分額: 3,400千円 (直接経費: 3,400千円); 2002年度: 3,400千円 (直接経費: 3,400千円)
• キーワード: Rigorous Review / Inspection / Formal Specification / Verification / Consistency / Validation / Specification Simulation / Data flow logic

研究概要

本年度には、最新のソフトウェアレビューあるいは検査の手法について全面的に調べたうえで、三つの問題点に集中して研究を行った。第一、形式的仕様の整合性を検証するために必要な性質(例えば、内部一致性、不変数とプロセスの一致性、充足性、及び統合一致性など)を定義し、親和性良い「レビュー木」、という言語を設計し、性質とレビュー木を基に厳密な仕様レビュー手法を開発した。この手法では、仕様の整合性をレビューするために、まず検証すべき性質を仕様要素から自動的に生成及び論理式で表示する。次は、生成された論理式からレビュー木へ自動的に変換する。その後、レビュー木により、基本的な論理部品をレビューする。最後は、レビューの結果を評価し、仕様にエラーがあるかどうかを判断する。第二、形式的仕様レビューの手段の一つとしての「仕様シミュレーション」技術を提案した。この技術を用いて、形式的仕様の各部品(例えば、プロセス、モジュール、クラス、CDFDなど)を動的にレビューすることができる。例えば、プロセスをシミュレーションするために、まず入力と出力変数に具体的な値を生成して、次はそれらの値を用いてプロセスを評価する。その結果により、プロセス仕様にエラーがあるかどうかを判断する。第三、仕様要素を統合してシステムの構造を反映するCDFDの正確性を厳密な分析するために必要な論理システムを設計した。この論理システムと前述した厳密なレビュー手法を統合することにより、実用的な分析技術の開発ができると考える。

研究成果

• [文献書誌] Shaoying Liu: "Formal Verification of Condition Data Flow Diegrams for Assurance of correct Network Protocols"Proceeding of International Conference on Advanced Information Networking and Applications, IEEE. March,2003(予定). (2003)
• [文献書誌] Shaoying Liu: "A Simulation Approach to Verification and Validation of Formal Specifications"Proceedings of First International Conference on Cyber World : Theory and Practice, IEEE. November. 113-120 (2002)
• [文献書誌] Shaoying Liu: "Capturing Complete and Accurate Requirements my Refinement"Proceeding of 8th IEEE International Conference on Engineering of Complex Computer Systems. December. 57-67 (2002)
• [文献書誌] Shaoying Liu: "A Rigorous Approach to Reviewing Formal Specifications"Proceeding of 27th IEEE/NASA International Software Engineering workshop. December(予定). (2002)
• [文献書誌] Shaoying Liu: "Integrating UML and SOFL for Object-Oriented Design"Proceeding of the Third International Conf. on Computer and Information Technology. Sept.. 92-98 (2002)
• [文献書誌] Shaoying Lin: "An Approach to Transforming Visual Formal Specifications to Java Programs"Proceeding of the Third International Conf. on Computer and Information Technology. Sept.. 116-123 (2002)
• [文献書誌] Shaoying Liu, Jin Song Dong: "Extending SOFL to Support Both Top-Down and Bottom-up Approaches"Proceeding of 2002 IEEE International Conference on Systems, Man, And Cybernetics. October. WAIQ2 (2002)
• [文献書誌] Shaoying Liu: "Developing Quality Software Systems using the SOFL Formal Engineering Method"Proceeding of 4th International Conference on Formal Engineeering Methods, LNCS 2495. LNCS2495. 3-19 (2002)
• [文献書誌] Shaoying Liu: "Formal Engineering Methods for Information Systems Development"Proceeding of Second International Conf. on INFORMATION. July. 148-154 (2002)