Synthèse des prospectives 2019

Introduction

Computing devices have become ubiquitous in everyday life, and this has led to growing concerns about their reliability. Because errors or malfunctions in these can have dramatic consequences, it is expected that these devices should be guaranteed to be safe, trusted, and have an explainable behavior. The goal of the teams in the "Formal methods, models and languages" research area is to understand the underlying semantic models and develop tools that can be used all the way from the rigorous design of computing devices to the formal proof that they behave as expected.

Research in formal methods is a long-term effort, usually with several decades spanning from early prototypes to robust products.

Societal challenges

System (software, hardware and cyber-physical) safety

Guaranteeing the safety of systems is a critical task in many domains. Due to the increasing heterogeneity and specialization of systems, their developers are faced with more and more complex and conflicting design issues, concerning the efficiency, inter-operability, trustability, and security of these systems. In particular, it has become near impossible to obtain an acceptable level of safety guarantees for a system by solely running a set of tests. Therefore, an increasing number of developers rely on formal tools to obtain this guarantee. Formal methods are also recommended and/or required for certain levels of certification. The rise of quantum technology has also led to new problems on program design, error correction and security issues.

Confidentiality

An increasing number of applications - especially those used in the construction of AI systems - are data- driven, and it is necessary to ensure that the data used by these applications does not compromise the privacy of individuals.

Adapting digital technology to the ecological transition

Digital technology needs to be adapted to the major challenge that is the ecological transition:

• Methods to better understand the environmental and societal impact of digital technology
• More important need for resiliency
• Need to recreate systems and infrastructures that require less energy, resources, maintainance, etc.

Challenges (Problems to solve)

Certified construction of systems

• use of formal methods
  • Propose and implement new formal languages for specifying, implementing, and verifying (concurrent) systems; this requires languages for both, system and property specifications
  • proof
  • test case generation

• integration in an industrial workflow
  • increase acceptance of languages
  • efficient and easy-to-use tools

Quantum information science

• A better understanding of possible correlations and how to exploit them.
• Circuit optimization
• How to model quantum control of operations
• How to use imperfect canals to improve tools for error detection and correction.

Explainability and accountability of embarked and cyber-physical systems

The increasing complexity and autonomy of CPS have made accountability and explainability requirements more crucial: in order to be socially acceptable, the behaviors of CPS must be explainable. This is particularly the case for systems in which decision making is based on AI, but it is not limited to this case. Along with safety, the respect - and violation - of properties such as security and privacy must be explainable. This explainability should in particular be used to understand were the blame lies from a legal point of view when a CPS malfunctions.

Research themes

Concepts, languages and tools for modelling and verifying complex systems

• Graph rewriting
• Automated reasoning
• Modern Process Calculi
• Modern Property specification languages
• Model-Checking, Equivalence Checking
• Library of verification components ("graph transformers") to facilitate reuse and easy development of new verification tools; this requires stable and rich interfaces
• rapid prototyping
• Automated test case generation
• Performance evaluation/prediction
  • connections between various modeling formalisms
  • unififed semantic models

Embedded IA

"Embedded IA" and more specifically "embedded machine learning". There are now FPGA and ASIC implementations for ML and CNN (convolutional neural networks), as well as multicore deployments.

Proof formalisation in applied mathematics and theoretical computer science

E.g.:

• Development of libraries of certified definitions
• Theorems and algorithms for financial mathematics, logic, etc.

Typed high-level languages for data science

The preparation of data (clean-up, requests, distributed handling, etc.) is of paramount importance in the construction of AI applications. Construction of type systems for the analysis and handling of data. Construction of analysis methods and optimized compilation for these languages; in particular for requests.