Qualifiable Software Parallelization for Multicore Avionics Systems (QSMA)
QSMA is a German civil aviation project supported by the Federal Ministry for Economic Affairs and Climate Action (BMWK) as part of the sixth civil aviation research program (LuFo VI). The project aims to establish a DO-178C/DO-330 qualifiable toolchain for multicore software development. The toolchain consists of the tools emmtrix Parallel Studio, AbsInt CompCert and AbsInt TimeWeaver. It is used in a demonstration project in which a TSO-C151b Terrain Avoidance and Warning System is being developed in accordance with DAL-C.
After substantatila progress in the domain of automation of aircrafts, the aviation industry is now turning to ‘intelligent’ and ‘networked’ flight. The development in the areas of digitalisation and artificial intelligence now requires powerful avionics systems. At the end of the exponential growth in clock frequencies, only multi-core processors can solve the ever-increasing computing demands of the next generation of airplanes. The problems here are potential software errors in parallel software (e.g. race conditions, deadlocks, synchronisation and communication errors), which cannot be detected even by full test coverage. Therefore, certification is very time-consuming, cost-intensive and currently de facto prevents the use of multicore processors for safety-critical applications.
In this project, the problem is to be addressed by means of a DO-178C qualifiable tool chain in order to eliminate recurring source code verification processes of parallel code. The parallelisation tool emmtrix Parallel Studio (ePS) is used to distribute sequential software on different cores and to achieve semantics preservation of sequential and parallel source code. Afterwards, the parallel source code is compiled with the formally verified optimising CompCert compiler to achieve semantics preservation down to the binary level. For temporal verification, the tools aiT (for statically predictable processors) and TimeWeaver (for more complex architectures) are used. In order to obtain an end-to-end qualifiable toolchain, this project will develop qualification kits for the ePS, TimeWeaver and CompCert tools, enabling their use for development projects in avionics based on DO-178C and related supplements. The toolchain will be used and evaluated in a demonstrator project according to DAL-C.