PHYLOG: a model-based certification framework

This paper describes PHYLOG, a framework intended to help certify the use of a multi-core in an aeronautical context. Specific guidelines for such systems have been published in a document, the MCP-CRI / CAST-32A, which provides a series of objectives to be fulfilled. To justify that an objective is indeed achieved, PHYLOG relies on structured graphical notations, recursively refining each objective by solving it using a strategy, itself having its own sub-objectives, until all that remains are evidences found either through the use of formal methods, as part of the design choices, or in external documentation. The PHYLOG framework includes such formal methods, providing the means to model the multi-core and to acquire further evidences through automatic analysis.