A Hypervisor Based Platform for the Development and Verification of Reliable Software Applications
摘要
In the XANDAR project, a holistic model-based toolchain has been formulated that follows the X-by-Construction (XbC) paradigm i.e., a “step-wise refinement from specifications to executable code” that results in systems with guaranteed non-functional properties. XANDAR defined also meta-model extensions, a library of safety, fault-tolerance, and security patterns, and investigated many further techniques for design automation, verification, and validation. In the project, the actual code generation procedure is performed by the XbC backend that efficiently performs the code optimizations, code parallelization, scheduling, mapping, and run-time system generation of the input software modules on the target platform ensuring that the predefined deadlines are met. This paper describes the main features of the XbC backend including the generation of the hypervisor configuration files that are customized for the target multicore platform. The use cases analyzed in XANDAR showcased that the proposed XbC backend was able to output acceptable solutions in an efficient manner.