Modeling Techniques aiming at Behavioral Verification for Developing Reliable Web Applications

旨在开发可靠 Web 应用程序的行为验证的建模技术

基本信息

批准号：
16500027
负责人：
YUEN Syouji
金额：
$ 1.86万
依托单位：
Nagoya University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2004
资助国家：
日本
起止时间：
2004 至 2006
项目状态：
已结题

项目摘要

We have investigated modeling techniques to improve reliability of Web applications in formally analyzing the behavior for correctness verification. Web applications are the software of information systems based on the World Wide Web technology. The fundamental difference of web applications is that it behaves inherently in the reactive manner in response from the environment. While a series of interaction, it is often required to maintain the local states. One of the reliability of web applications is that the application behaves as expected for all possible interactions without any deadlock or any unintended state transitions. In this view of reliability, we have investigated following topics: (1) A behavioral model called "Web Automaton" where a label attache to a transition is a request from the environment accompanied with data constraints, (2) a GUI design by a programming language with the name passing capability, (3) Asynchronous local pi-calculus over the programming language Haskell, and (4) a quality assurance technique considering a well behaved tree-like structure focusing on easing to avoid client-side script errors. For the web automata model, we proposed a systematic testing generation of consistent series of requests. Application of name-passing mechanism in the Nepi programming language illustrates the simplicity of the behavioral aspect in the communicating processes. PiMonad is a light-weight implementation of the local asynchronous pi-calculus over, Haskell. PiMonad enables the integrated framework of functional programming with network programming. The quality assurance model aims the quality improvement of the client-side scriptsThroughout this research, we have investigated each element technology based on the integrated view of communicating processes. As the future work, we will proceed to compose and integrate these techniques into web applications

我们研究了建模技术，以提高 Web 应用程序在正式分析行为以进行正确性验证时的可靠性。 Web应用程序是基于万维网技术的信息系统软件。 Web 应用程序的根本区别在于它本质上以反应方式响应环境。在进行一系列交互的同时，往往需要维护本地状态。 Web 应用程序的可靠性之一是应用程序对于所有可能的交互都按预期运行，不会出现任何死锁或任何意外的状态转换。从可靠性的角度来看，我们研究了以下主题：(1) 一种称为“Web 自动机”的行为模型，其中附加到转换的标签是来自环境的请求，并伴有数据约束，(2) 通过编程进行 GUI 设计具有名称传递功能的语言，（3）基于编程语言 Haskell 的异步本地 pi 演算，以及（4）考虑行为良好的树状结构的质量保证技术，重点是轻松避免客户端脚本错误。对于网络自动机模型，我们提出了一系列一致请求的系统测试生成。 Nepi 编程语言中名称传递机制的应用说明了通信过程中行为方面的简单性。 PiMonad 是 Haskell 本地异步 pi 演算的轻量级实现。 PiMonad 支持函数式编程与网络编程的集成框架。质量保证模型旨在提高客户端脚本的质量。通过本研究，我们基于通信过程的集成视图研究了各个要素技术。作为未来的工作，我们将继续将这些技术组合并集成到 Web 应用程序中