We are developing techniques of system verifications using formal methods in the designing phase of software development in industry. As a case study, we applied a model checking technique to specifications of an embedded system under development in a company. Model checking was proceeded in parallel with the designing process in the company and was completed in a reasonably short term. As a result of this collaboration, we could successfully detect six unknown bugs. Consequently our technique could contribute to improve the quality of the developing system and to cut down its developing cost. Thus this case study shows that an application of model checking technique to software specifications is feasible and effective.
|
|
|
Comparing a conventional method and a new method
|
|
| Relational Information |
|

|
AIST Today Vol. 3, No.10 (2003) 11
|