FORMED: Bringing Formal Methods to the Engineering Desktop
Technical Report,01 Nov 2013,30 Nov 2015
BAE SYSTEMS Burlington United States
Pagination or Media Count:
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.