状態爆発する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）使用Strut创建的基于组件的Web应用程序的各种示例问题。我们将从规模的角度研究有用性。我们还将以一种使用组件划分的一般方式来打破由状态爆炸等引起的应用限制障碍。克服状态爆炸的一种方法是将系统视为基于组件的系统，将系统组成，并将整个系统的范围划分到整个系统中，并将其分配到整个系统中，并且在整个组件中均具有验证。这样的组件和设计。此方法重点介绍了这一点。，我们提出了一种在设计阶段中间有效利用产品（UML描述，Web过渡图）的方法，并实际创建了一个检查工具来研究其有效性。这里的挑战是设计一种方法来维持可伸缩性，而不会在验证整个系统时失去组件划分的好处，并通过计算机支持有效地对其进行适当的模型。在以前的研究项目中，我们提出了一种方法，以有效地验证实时UML描述的基于组件的系统和支柱的时间QoS属性。已经对如何执行页面过渡和模型检查所描述的Web应用程序的内部行为进行了研究。在设计实时系统的基于组件的时间属性的设计验证时，我们证明了它是可验证的，例如Bang＆Olulfsen的协议。我们已经证明，Web应用程序可以应用于在公司新员工培训中创建的在线商店的设计。这表明这种方法是有效的。对于后者，我们在Eclipse上开发了一个插件。