Generating Verified Java Components Through RESOLVE

Document Type

Conference Proceeding

Publication Date

11-2-2009

Description

For software components to be reused with confidence, they must be correct. Unlike testing, formal verification can be used to certify that a component will behave correctly regardless of context, as long as that context satisfies component assumptions. Some verification systems for developing correct components in languages such as Java are simplified to be practical, but are not complete. Other systems that account for necessary semantic complications arising from underlying reference behavior demand non-trivial specification and verification. This paper describes an alternative. Under this approach, reusable components are specified, implemented, and verified in RESOLVE, a language with clean semantics, and are translated to Java. To improve confidence in the verification process, we are currently re-engineering the RESOLVE verification system itself with generated verified components.

Share

COinS