FORMED: Bringing Formal Methods to the Engineering Desktop

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 2016
Accession Number
AD1004403

Entities

People

  • Greg Eakman
  • Howard Reubenstein
  • John Wiegley
  • Mitesh Jain
  • Panagiotis Manolios

Organizations

  • BAE Systems

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Air Force
  • Air Force Research Laboratories
  • Application Software
  • Computer Programming
  • Computer Programs
  • Contracts
  • Engineering
  • Formal Languages
  • Language
  • Lisp Programming Language
  • Programming Languages
  • Software Design
  • Software Development
  • Specifications
  • Standards
  • Translations
  • Verification

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Distributed Systems and Data Platform Development