Modeling Techniques aiming at Behavioral Verification for Developing Reliable Web Applications
| Project/Area Number |
16500027
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Computer system/Network
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
YUEN Syouji Nagoya University, Graduate School of Information Science, Associate Professor, 大学院情報科学研究科, 助教授 (70230612)
|
|---|
| Project Period (FY) |
2004 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2005: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2004: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | Web applications / Communicating Processes / Process algebra / pi-calculus / Internet integration / Programming languages / Haskell / Type systems / 通信ブロセスモデル / 形式意味論 / プログラム検証 / 代数的意味論 / タイムアウト処理 / WWW / 並行計算 / ネットワークプログラミング |
|---|
| Research Abstract |
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 scripts
Throughout 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
|
Report
(4 results)
Research Products
(33 results)
