B4L4 falls within the context of projects related to the definition of secure platform architectures. The partners are:
- ST Microelectronics: AST R&D team at Rousset
- ENST: LabSoc
The project relates to the formal modelling of a secure operating system and the validation of its development.
B Method is used to model the system and the APIs for the various servers that compose the OS. Studies on the use of these models as test oracles are also conducted. The CEA is studying the applicability of the Caveat tool in the context of operating systems.