Generating verifiable Java code from verified PVS specifications

Abstract

The use of verification tools to produce formal specifications of digital systems is commonly recommended, especially when dealing with safety-critical systems. These formal specifications often consist of segments which can automatically be translated into executable code. We propose to generate both code and assertions in order to support verification at the generated code level. This is essential (and possible) when making modifications to the implemented code without revering to the verification tool, as the formal verification can be performed directly at the level of the adjusted code. As a result of a feasibility study on this approach, we present a prototype of a code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into Java annotated with JML assertions. To illustrate the tool's functionality a verified communication protocol from the NASA AirStar project is taken and a reference implementation in Java is generated. Subsequently, we experiment with verification on the Java level in order to show the feasibility of proving the generated JML annotations. In this paper we report on our experiences in this feasibility study. © 2012 Springer-Verlag.