A Formal Approach to the Provably Correct Synthesis of Mission Critical Embedded Software for Multi Core Embedded Platforms

Abstract

This is the final report on the findings of the AFRL funded project "A Formal Approach to the Provably Correct Synthesis of Mission Critical Embedded Software for Multi-core Platforms." In this work we enhanced the theory of a formal modeling language based specifications, namely MRICDF. We demonstrated an implementation of a software specification and code synthesis tool based on MRICDF. The work entails new synthesis algorithms, characterization of specifications, formal proof techniques for proving the correctness preservation property of the refinement steps in our step-wise refinement oriented synthesis technique, multi-core code synthesis, endowing the specification with platform specific worst case execution times to check real-time schedulability, and some case studies.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 2014
Accession Number
ADA602193

Entities

People

  • B. Jose
  • J. Ouy
  • M. Kracht
  • M. Nanjundappa
  • Miles Anderson
  • Shivakant Shukla

Organizations

  • Virginia Tech

Tags

Communities of Interest

  • Energy and Power Technologies
  • Engineered Resilient Systems
  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Air Force
  • Air Force Research Laboratories
  • Algorithms
  • Case Studies
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Control Systems
  • Engineers
  • Language
  • Operating Systems
  • Programming Languages
  • Software Design
  • Standards
  • Systems Engineering
  • Unmanned Aerial Vehicles

Fields of Study

  • Computer science
  • Engineering

Readers

  • Distributed Systems and Data Platform Development
  • Software Engineering.