Expression and validation of logical and physical security properties for critical computer systems.

Summary Within the framework of our research activities, we are interested in the security of so-called critical systems (which, in case of failure, can cause serious damage to people or property). The security of such systems requires the expression of recommendations related to security. These recommendations can come from a client's request (clauses in the specifications), from the state of the art, from a legal reference (standards, decrees, orders, etc.) or from studies on the consequences of system failures on the environment, people, the company's brand image, etc. From the recommendations introduced in the customer's specifications, it is therefore possible to identify "requirements". It will then be necessary to demonstrate that these requirements are taken into account during the entire system realization cycle. In this thesis, we propose a method and examples of implementation based on the identification, expression and verification of security-related requirements.