Accession Number:

AD1004401

Title:

Specification Improvement Through Analysis of Proof Structure (SITAPS): High Assurance Software Development

Descriptive Note:

Technical Report,01 Sep 2013,30 Sep 2015

Corporate Author:

BAE Systems Burlington United States

Personal Author(s):

• Reubenstein,Howard
• Eakman,Greg
• Hawkins,Tom

Report Date:

2016-02-01

Pagination or Media Count:

24.0

Abstract:

Formal software verification methods and tools have made significant progress in their ability to model software designs and prove correctness theorems about the systems modeled. General adoption of these techniques has had limited penetration in the software development community. Two interrelated causes may account for barriers to adoption. First, many tools prove properties about models of the system as opposed to the actual implementation. Software engineers ultimately need to produce performant software implementations and therefore they are primarily concerned with properties of their implementations. Second, while it is crucial that formal derivation processes do not introduce deviations from the specification or vulnerabilities a domain independent requirement engineers also need to verify application and domain specific properties in building their implementations. The SITAPS Specification Improvement Through Analysis of Proof Structure project described in this report explores techniques that can be used to obtain greater domain and application specific assurances.

Descriptors:

• SOFTWARE ENGINEERING
• QUALITY ASSURANCE
• COMPUTER PROGRAM VERIFICATION
• validation

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE