Accession Number : AD1004403


Title :   FORMED: Bringing Formal Methods to the Engineering Desktop


Descriptive Note : Technical Report,01 Nov 2013,30 Nov 2015


Corporate Author : BAE SYSTEMS Burlington United States


Personal Author(s) : Reubenstein,Howard ; Eakman,Greg ; Wiegley,John ; Manolios,Panagiotis ; Jain,Mitesh


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/1004403.pdf


Report Date : 01 Feb 2016


Pagination or Media Count : 45


Abstract : FORMED integrates formal verification into software design and development by precisely defining semantics for a restricted subset of the Unified Modeling Language and transforming application models into both an ACL2s formal specification for analysis and Java code for deployment. Correspondence testing verifies consistent translation and executable behavior between the formal and deployed implementations. Key properties addressed include termination, input-output contract satisfaction and absence of null pointer dereferences.


Descriptors :   COMPUTER PROGRAM VERIFICATION , validation , SPECIFICATIONS , SOFTWARE ENGINEERING


Distribution Statement : APPROVED FOR PUBLIC RELEASE