Modeling Techniques aiming at Behavioral Verification for Developing Reliable Web Applications

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

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