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

摘要

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.