| Current Works |
| [Collection and Systematization of know-how and examples to apply Model-checking in actual software development process] |
| Using know-how drawing from experiences and similar examples is very effective to apply Model-checking in actual software developing process. Attempting Model-checking to software using only fundamental knowledge is loss of brain power and work-time. We are collecting Model-checking examples in software development process and systematize the know-how from examples. We also open some example to the public for the popularization of Model-checking. |
|
|
| [Development of guide-book for software engineer (not for researcher) containing practical know-how in Japanese] |
| Most of papers and publications about Model-checking are written in English. They are hard to understand for most of Japanese engineers. It is wonderful that Model-checking seminars or workshops in Japanese began to hold after 2004. We are developing guide-book in Japanese. Our guide-book is for beginners who study fundamentals of Model-checking in some seminars and containing practical know-how which prevents unnecessary toil and troubles on actual software model-checking. |
|
|
| [Development of support software to SMV(*)] |
Model-checking needs test program written in modeling language specific to model-checkers.
Modeling language is not difficult for programmers to verify small examples and small systems.
But model become large size, describing the test program in modeling language is very hard even for the well experienced model checking engineer. So, we are developing the model building tool "Support Software to SMV". This "Support Software to SMV" is useful for engineers who do not write programs |
|
| (*)SMV: a symbolic model checker for CTL developed and distributed in CMU |
|
|
|
