Practices for formal models as documents: Evolution of VDM application to “Mobile FeliCa” IC chip firmware

Abstract

This paper reports on the application of VDM to the development of the third generation of firmware for the Mobile FeliCa IC chip. The practices of VDM were improved by incorporating the experience gained in the previous development. The primary focus was maintainability and understandability, as the VDM specification was used as the sole reference document for various development activities. The resulting improvements eliminated deficiencies caused by misunderstandings, while keeping costs similar to before.