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

Report Date:

2016-02-01

Pagination or Media Count:

45.0

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.

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE