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

自动化正式规范和严格的程序审查的研究

• 批准号: 14019081
• 负责人: 劉 少英
• 金额: $ 2.18万
• 依托单位: Hosei University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14019081/
• 关键词: Rigorous Review; Inspection; Formal Specification; Verification; Consistency; Validation; Specification Simulation; Data flow logic

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

This year, the latest software is available for investigation, comprehensive adjustment, and focused research on three problem points. The first is to define the necessary properties (e.g., internal consistency, consistency, sufficiency, and integration consistency) of the formal integrity model, to define the affinity, to design the language, to develop the properties, to design the basis, and to develop the confidentiality model. This technique is based on the integration of functions, functions, and functions, as well as the automatic generation and logical expression of functions. The second generation logic expression is automatically changed. Later, basic logic components can be displayed at any time. Finally, the results of the review, the official review, the final review. Second, the technical proposal of the form of "service system" is proposed. This technology is applied to all parts of the form (e.g., mobile, mobile, CDFD). For example, the number of input and output is determined by the number of input and output. The result of the test is that Third, the integration of the elements of the system structure reflects the legitimacy of CDFD, and the necessary logic of the system design. The logic of this system is based on the integration of the aforementioned analytical techniques and the development of practical analytical techniques.

项目成果

Shaoying Liu: "Formal Engineering Methods for Information Systems Development"Proceeding of Second International Conf. on INFORMATION. July. 148-154 (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：“使用 SOFL 形式工程方法开发质量软件系统”第四届形式工程方法国际会议论文集，LNCS 2495。LNCS2495。

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：“用于保证正确网络协议的条件数据流图的形式验证”高级信息网络和应用国际会议论文集，IEEE，2003 年 3 月（预定）。

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：“Capturing Complete and Accuracy Demand my Refinement”第八届 IEEE 复杂计算机系统工程国际会议论文集。

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、Jin Song Dong：“扩展 SOFL 以支持自上而下和自下而上的方法”2002 年 IEEE 国际系统、人与控制论会议论文集。