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.
Citation Information
Smith, Hampton; Harton, Heather; Frazier, David; Mohan, Raghuveer; and Sitaraman, Murali. 2009. Generating Verified Java Components Through RESOLVE. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol.5791 LNCS 11-20. https://doi.org/10.1007/978-3-642-04211-9_2 ISSN: 0302-9743 ISBN: 3642042104,9783642042102