From Formal Methods to Executable Code
Peter M. Musial · DSpace@MIT (Massachusetts Institute of Technology) · 2012
In this paper we will discuss one approach to achieving software reliability. In particular, where software systems are modeled using a formal mathematical framework that is used to verify their behaviors. Once verified these are translated to executable code. Formal system specifications and their behavior analysis are valuable tools that should be at the disposal of the software developers, especially when dealing with systems exhibiting high levels of concurrency. However, theoretically sound specifications have a limited impact, unless tools exist that automatically transform these specifications from high level representation to executable code. One challenge that arises with this approach is to provide a comprehensive and usable set of abstractions (such as files, network protocols, console, etc.) that will serve as building blocks of the abstract software models. Another difficulty is to ensure performance of the generated code. Finally, the translation process has to be formally verified to result in executable code that can be deemed as reliable and correct by its construction.