| Project/Area Number |
12680350
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | NARA INSTITUTE OF SCIENCE AND TECHNOLOGY |
|---|
Principal Investigator |
SEKI Mhiroyuki NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORMATION SCIENCE, PROFESSOR, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKATA Yoshiaki NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORMATION SCIENCE, ASSISTANT PROFESSOR, 情報科学研究科, 助手 (60294279)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 2001: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2000: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | USER INTERFACE / INTERACTIVE SYSTEM / FORMAL VERIFICATION / PROTOTYPE GENERATION / TASK DIAGRAM / ALGEBRAIC SPECIFICATION / ABSTRACT SEQUENTIAL MACHINE / ソフトウェア設計法 |
|---|
| Research Abstract |
A formal method for interactive system design is proposed. In the proposed method, a task model is constructed by a task flow diagram. The semantics of a task flow diagram is formally defined by LOTOS, which is a formal specification language based on the process algebra. A task flow diagram is refined by decomposing each task into several subtasks which represent system actions and user actions. Next a formal verification method for a task model is proposed. In our method, the LOTOS specification derived from a task flow diagram is verified by a model checking-based verification tool CADP. We also present an automatic prototype generation method which translates a task model into an HTML and a CGI program.
A formal description method of user interface (UI) based on a subclass of algebraic specifications called abstract sequential machine (ASM) specifications is proposed and a prototype generation method from an ASM specification is discussed We introduce an abstract window system (AWS), which is a simple multiprocess model where each UI module behaves asynchronously by sending or receiving messages. Each UI module is modeled as a component of the AWS and is defined by an ASM specification. We implemented a compiler which translates an ASM specification of UI into a Java program. Experiences with the compiler showed the effectiveness of the proposed method.
|
