状態爆発する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上のプラグインを開発した.

在信息爆炸的信息社会中，利用逻辑和数学手段保证软件的安全性和有效性变得越来越重要。软件模型检验作为这些方法之一近年来受到人们的关注。本研究，软件模型的适用范围检查是否按比例缩放。本研究的目的是从性能的角度进行研究。具体来说，目的是（1）验证实时系统基于组件的时间属性的设计，以及（2）基于组件的 Web 应用程序的各种示例使用 Struts 创建用于软件模型检查。我们将应用这种方法，并从规模的角度检验它的有用性。我们还将设计一种通用方法，利用组件划分来突破状态爆炸等造成的适用性壁垒。克服状态爆炸的一种方法是编写一个系统由多个子系统组成。它是一个基于组件的系统，问题分为各个组件的验证和整个系统的验证。一般在设计软件系统时，很自然地将设计划分为这样的组件，这种方法侧重于这一点。，我们提出了一种有效利用设计阶段的中间产品（UML描述、WEB转换图）的模型检查方法，创建了一个实际的检查工具，并调查了其有效性。这里的挑战是在进行整体验证时，有可能提高可扩展性，同时又不失去划分组件的好处。该研究项目的目的是设计一种方法来维护系统并通过计算机支持方法有效地执行适当的建模，以使用 Struts 验证时间 QoS 属性。我们已经取得了对书面 Web 应用程序的页面转换和内部操作进行模型检查的方法的研究成果。在实时系统基于组件的时间属性的设计验证中，我们发现可以使用 Bang & Olulfsen 的协议进行验证例如，对于Web应用程序，我们展示了它可以应用于企业新员工培训期间创建的在线商店的设计。我们认为，这表明这种方法对于后者是有效的，我们开发了一个插件。对于 Eclipse。