Timo Nummenmaa (MSc) is a PhD student and researcher at the University of Tampere, Finland. His main research area is the utilization of executable formal specifications in software development and game development.
Software Verification with Next Generation DisCo Specifications
Timo Nummenmaa1, Tommi Mikkonen2
- 1School of Information Sciences, University of Tampere, Kanslerinrinne 1, FI-33014, Tampere, Finland timo.nummenmaa@uta.fi
- 2Department of Software Systems, Tampere University of Technology, Korkeakoulunkatu 1, FI-33720, Tampere, Finland tommi.mikkonen@tut.fi
Abstract
In this paper we present a method for verifying software with formal executable specifications throughout its lifecycle. The key part in the method is the transition from specification to implementation. In our solution, the specification stays as an integral part of the implementation throughout its life-cycle and the software is verified against it during both initial implementation and also maintenance. The solution relies on the use of a database-driven version of the DisCo specification system for developing the software.