| Project/Area Number |
16300007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | KYUSHU UNIVERCITY |
|---|
Principal Investigator |
ARAKI Keijiro Kyushu University, Graduate School of Information Science and Electrical Engineering, Professor, 大学院システム情報科学研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
FUKUDA Akira Kyushu University, Graduate School of Information Science and Electrical Engineering, Professor, 大学院システム情報科学研究院, 教授 (80165282)
KUSAKABE Shigeru Kyushu University, Graduate School of Information Science and Electrical Engineering, Associate Professor, 大学院システム情報科学研究院, 助教授 (70234416)
CHANG Han-Myung Nanzan University, Faculty of Mathematical Sciences and Information Engineering, Associate Professor, 数理情報学部, 助教授 (90329756)
NAKANISHI Tsuneo Kyushu University, Graduate School of Information Science and Electrical Engineering, Associate Professor, 大学院システム情報科学研究院, 助教授 (70311785)
OMORI Yoichi Kyushu University, Graduate School of Information Science and Electrical Engineering, Research Associate, 大学院システム情報科学研究院, 助手 (20309727)
|
|---|
| Project Period (FY) |
2004 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥14,300,000 (Direct Cost: ¥14,300,000)
Fiscal Year 2006: ¥4,200,000 (Direct Cost: ¥4,200,000)
Fiscal Year 2005: ¥5,000,000 (Direct Cost: ¥5,000,000)
Fiscal Year 2004: ¥5,100,000 (Direct Cost: ¥5,100,000)
|
|---|
| Keywords | system modeling / formal specification / embedded software / manifold description and analysis / case studies / highly reliable systems / behavioral analysis / aspect-orientation / アスペクト志向 / システム特性 / モデル検査 |
|---|
| Research Abstract |
In this research project, we made several case studies of describing and modeling systems with formal specification languages VDM-SL and VDM++ which include embedded software systems such as elevator control systems, contactless IC card systems, industrial robot systems and so on. We also intended to make the system models reusable. To this end, we proposed a way to find exceptional features from normal features based on feature diagrams and fault trees. Besides, we proposed a way to detect aspect interference in aspect-oriented programs.
We proposed a method to develop high-quality software systems efficiently using abstract and rigorous formal specifications together with comprehensive diagrammatic system descriptions. We use VDM and UML to develop systems from abstract system models and specification through C++ programs. We showed full assurance of practical effectiveness of combining formal and informal description tools through above case studies.
We presented a method for analyze and verify the system behaviors with finite state machine models generated from system description with VDM-SL. We apply model checking approach to analyze the properties of system behaviors. We also presented a new concept to describe control systems with Petri-nets. We introduced a meta-level attributes to transitions and places to express abstract control features other than ordinal actions. With this new concept, complicated Petri-net systems would be reduced to smaller systems and become more understandable.
|
