权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

状態爆発するWEBアプリケーションに対するソフトウェアモデル検査

状态爆炸 Web 应用程序的软件模型检查

基本信息

批准号：
18049054
负责人：
岡野浩三
金额：
$ 1.02万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2006
资助国家：
日本
起止时间：
2006 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-18049054/
关键词：
SPIN UML OCL WEB Struts UPPAAL timelines QoS

项目摘要

ソフトウェアの安全性妥当性を論理的数学的な手段で保証することは情報爆発する情報社会にとってますます重要である.その手段の1つとしてソフトウェアモデル検査が近年注目を浴びている.本研究は,ソフトウェアモデル検査の有用性適用限界を規模に対するスケーラビリティの観点から調べることをその目的とする.具体的には(1)実時間システムのコンポーネントベースの時間性質の設計検証と(2)Strutsを用いて作成されたコンポーネントベースのWEBアプリケーションの各種例題に対して,ソフトウェアモデル検査を適用し,規模の観点から有用性を調べていく.また,状態爆発などによって生じる適用限界の壁をブレークスルーするための方法論をコンポーネントの分割を用いた一般性のある形で考案していく.状態爆発を克服する1つの方法はシステムを複数のサブシステムからなるコンポーネントベースシステムとしてとらえ,各コンポーネントの検証とシステム全体の検証に問題を分割することである.一般にソフトウェアシステムを設計する際,そのようなコンポーネントに分割して設計を行うことは自然なことである.本手法はそのことに着目し,設計段階の途中生産物(UML記述,WEB遷移図)を有効利用し,モデル検査する方法を提案し,実際に検査ツールを作成し,その有効性を調べた.ここでの課題は,システム全体の検証を行う際,コンポーネント分割したメリットを失うことなく,スケーラビリティを維持する方法を考案することや,計算機支援を通じて,適切なモデル化を効率良く行うことである.これまでのこの研究プロジェクトでは,UML記述されたコンポーネントベースの実時間システムに対して,効率よく時間QoS性質を検証する方法論とStrutsで記述されたWEBアプリケーションに対するページ遷移や内部動作のモデル検査を行う方法について研究成果を挙げてきた.実時間システムのコンポーネントベースの時間性質の設計検証においては,Bang＆Olulfsenのプロトコル例題に対して,検証可能なことを示した.WEBアプリケーションについては企業新人研修で作成したオンラインショップの設計に対して適用可能であることを示した.このことはこのアプローチが有効であることを示していると考える.また後者についてはEclipse上のプラグインを開発した.

The security and appropriateness of software are guaranteed by logical mathematical means, which are important for the information society. A survey of recent years has focused on the development of new technologies. The purpose of this study is to examine the usefulness of the software and its application limits in terms of scale and purpose. Specifically,(1) the design model of the time property of the system;(2) the application of Struts to the design of the system;(3) the application of Struts to the design of the system;(4) the application of Struts to the design of the system;(5) the application of Struts to the design of the system;(6) the application of Struts to the design of the system;(7) the application of Struts to the design of the system;(8) the application of Struts to the design of the system;(9) the application of Struts to the design of the system; and (10) the application of Struts to the design of the system. The methodology of the application of boundary conditions to the division of conditions is general. The method of solving the problem of state explosion is to divide the problem of all kinds of problems into several kinds of problems. In general, the design of the system is based on the design of the system, and the design of the system is based on the natural design. This method is aimed at designing products (UML description,WEB migration) in the middle of the stage. It is effective to use the method of investigation, and to make investigation in practice. It is effective to investigate. The problem is that when the whole system is tested, the system is divided into two parts, and the method of maintaining the system is tested. The computer support system is connected, and the system is optimized. This research is based on UML description of the time system of QoS properties, and Struts description of the methodology of QoS properties verification. The design of the time property of the time series is shown in the example of Bang& Oulfsen.WEB The design of the time series is shown in the example of Bang& Oulfsen. This is a good time to express your feelings and thoughts. The latter is the case with Eclipse.