Accession Number : ADA602193


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


Descriptive Note : Final rept. Oct 2010-Oct 2013


Corporate Author : VIRGINIA POLYTECHNIC INST AND STATE UNIV BLACKSBURG


Personal Author(s) : Shukla, S ; Nanjundappa, M ; Anderson, M ; Jose, B ; Kracht, M ; Ouy, J


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a602193.pdf


Report Date : Apr 2014


Pagination or Media Count : 94


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.


Descriptors :   *SOFTWARE ENGINEERING , EMBEDDED SYSTEMS


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE