2001 Fiscal Year Final Research Report Summary
Basic Study on Formal Approaches to Systematic Development Methods of High-Quality Embedded Systems
| Project/Area Number |
12680354
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
ARAKI Keijiro Kyushu University, Graduate School of Information Science and Electrical Engineering, Professor, 大学院・システム情報科学研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MOCHIO Koji Chikushi Women's University, Faculty of Literature, Lecturer, 文学部, 講師 (60331013)
CHANG Han-myun Nanzan University, Faculty of Mathematical Sciences and Information Engineering, Lecturer, 数理情報学部, 講師 (90329756)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Keywords | Formal Specification / Domain Modeling / Formal Methods / Statecharts / System Behavior Description / Formal Specification Testing / Case Studies / Diagram Analyzer |
|---|
| Research Abstract |
We constructed system models in several case studies of practical embedded systems in the real world, and described their formal specification. We have been using formal specification languages, Z and VDM-SL (Vienna Development Method - Specification Language). At different abstraction levels and different purposes in system development, we illustrated effective ways to describe and analyze the systems.
As a case study, we made an abstract model for vending machines, and showed a systematic way to enhance it to more advanced and complicated models. We also derived a formal description for a controller of a vending machine from its informal and ambiguous operation manual. We described both a functional description in formal specification languages and a dynamic description of its behavior with Statecharts. We invented a systematic way to derive statecharts from a formal specification in VDM-SL, and then we proposed a systematic approach to get these two kinds of descriptions which are consistent and complementary each other.
We also developed a generic analysis tool for diagrams which are used frequently in system design and analysis. We applied it to a variety of problems and showed its usefulness especially in querying constrained paths with specific attributes. We investigated the extension of the diagram analyzer to deal with Statecharts and analyze dynamic behaviors of embedded systems.
|
