2005 Fiscal Year Final Research Report Summary
Construction and verification of problem models in behavioral specifications
| Project/Area Number |
15300007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Japan Advanced Institute Science and Technology |
|---|
Principal Investigator |
FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology, School of Information Science, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
NAKAMURA Masaki Japan Advanced Institute of Science and Technology, School of Information Science, Associate, 情報科学研究科, 助手 (40345658)
|
|---|
| Project Period (FY) |
2003 – 2005
|
| Keywords | problem model / system verification / system safety / formal methods / behavioral specification / requirement specification / CafeOBJ |
|---|
| Research Abstract |
The following two important problems about construction and verification of problem models are investigated :
(1) How to set an appropriate abstraction level in constructions of problem models and/or specifications.
(2) How to combine interactive theorem proving technique and automatic searching based model checking technique in a collaborative way.
Based on empirical studies on constructing and verifying problem models in several areas like railway signaling systems, component software systems, secure authentication systems, and etc., we got the following results.
(1) Based on language constructs supported by CafeOBJ language, we have found that the distinction of abstract data types and abstract process types plays an important role in setting appropriate level in modeling/specification phase. Modeling/specification of process types are found to be complex and difficult than abstract data types, and we propose OTS (Observational Transition System) as a simple but powerful scheme for modeling/specifying process types. OTS is shown to be an effective and usable scheme for process types after applying it to several cases.
(2) After studying several cases we have done, we found that (i) interactive theorem proving is more effective for proving some property hold, and (ii) automatic model checking is more effective for proving the some property does not hold (i.e. for finding counter examples). Based on this observation, we designed and developed an interactive tool which can support interactive proof (of proving some property hold) by finding counter examples with a model checking technique.
|
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Proof scores in the OTS/CafeOBJ method2003
Author(s)
Ogata, K., Futatsugi, K.
-
Journal Title
Proceedings of the 6th IFIP WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2003), Lecture Notes in Computer Science (Springer) Vol.2884
Pages: 170-184
Description
「研究成果報告書概要(欧文)」より
