Modeling Techniques aiming at Behavioral Verification for Developing Reliable Web Applications

点击翻译按钮获取中文摘要

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