Dependable software through higher-order strategic programming.

Winter, Victor Lono (University of Nebraska at Omaha) ; Fraij, Fares (University of Texas at El Paso) ; Roach, Steve (University of Texas at El Paso)

Sandia National Laboratories

关键词: Modifications;    99 General And Miscellaneous//Mathematics, Computing, And Information Science;    Safety Programming (Electronic Computers);    Programming;    Software Maintenance.;   

DOI  :  10.2172/918741
RP-ID  :  SAND2004-0868
RP-ID  :  AC04-94AL85000
RP-ID  :  918741

美国|英语

来源: UNT Digital Library

【 摘 要 】

Program transformation is a restricted form of software construction that can be amenable to formal verification. When successful, the nature of the evidence provided by such a verification is considered strong and can constitute a major component of an argument that a high-consequence or safety-critical system meets its dependability requirements. This article explores the application of novel higher-order strategic programming techniques to the development of a portion of a class loader for a restricted implementation of the Java Virtual Machine (JVM). The implementation is called the SSP and is intended for use in high-consequence safety-critical embedded systems. Verification of the strategic program using ACL2 is also discussed.