Synthèse des prospectives 2019 - Historique des versions

Serwe : /* Confidentiality */

2019-03-11T08:32:34Z

Confidentiality

← Version précédente		Version du 11 mars 2019 à 08:32
Ligne 13 :		Ligne 13 :
	=== Confidentiality ===		=== 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.		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 ===		=== Adapting digital technology to the ecological transition ===

Serwe : /* Concepts, languages and tools for modelling and verifying complex systems */

2019-03-11T08:31:36Z

Concepts, languages and tools for modelling and verifying complex systems

← Version précédente		Version du 11 mars 2019 à 08:31
Ligne 55 :		Ligne 55 :
	* Modern Property specification languages		* Modern Property specification languages
	* Model-Checking, Equivalence Checking		* Model-Checking, Equivalence Checking
	* Library of verification components to facilitate reuse and easy development of new verification tools; this requires stable and rich interfaces		* Library of verification components ("graph transformers") to facilitate reuse and easy development of new verification tools; this requires stable and rich interfaces
	* rapid prototyping		* rapid prototyping
	* Automated test case generation		* Automated test case generation

Serwe : /* Research themes */

2019-03-11T07:47:10Z

Research themes

← Version précédente		Version du 11 mars 2019 à 07:47
Ligne 53 :		Ligne 53 :
	* Automated reasoning		* Automated reasoning
	* Modern Process Calculi		* Modern Process Calculi
			* Modern Property specification languages
	* Model-Checking, Equivalence Checking		* Model-Checking, Equivalence Checking
			* Library of verification components to facilitate reuse and easy development of new verification tools; this requires stable and rich interfaces
	* rapid prototyping		* rapid prototyping
	* Automated test case generation		* Automated test case generation
	* ~~performance~~ evaluation/prediction		* Performance evaluation/prediction
			** connections between various modeling formalisms
			** unififed semantic models

	=== Embedded IA ===		=== Embedded IA ===

Serwe : /* Certified construction of systems */

2019-03-11T07:42:48Z

Certified construction of systems

← Version précédente		Version du 11 mars 2019 à 07:42
Ligne 32 :		Ligne 32 :

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

	=== Quantum information science ===		=== Quantum information science ===

Serwe : /* Certified construction of systems */

2019-03-11T07:37:54Z

Certified construction of systems

← Version précédente		Version du 11 mars 2019 à 07:37
Ligne 27 :		Ligne 27 :

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

Serwe : /* Certified construction of systems */

2019-03-11T07:35:57Z

Certified construction of systems

← Version précédente		Version du 11 mars 2019 à 07:35
Ligne 27 :		Ligne 27 :

	* use of formal methods		* use of formal methods
			** propose and implement new formal languages for specifying, implementing, and verifying (concurrent) systems
	** modeling and verification
	** proof		** proof
	** test case generation		** test case generation

Serwe : /* Introduction */

2019-03-11T07:35:00Z

Introduction

← Version précédente		Version du 11 mars 2019 à 07:35
Ligne 2 :		Ligne 2 :

	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.		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 ==		== Societal challenges ==

Mechenim le 6 mars 2019 à 21:36

2019-03-06T21:36:54Z

← Version précédente		Version du 6 mars 2019 à 21:36
Ligne 31 :		Ligne 31 :
	* integration in an industrial workflow		* integration in an industrial workflow

	=== ~~Error~~ ~~correction~~ ===		=== 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 ===		=== Explainability and accountability of embarked and cyber-physical systems ===
Ligne 59 :		Ligne 64 :
	* Theorems and algorithms for financial mathematics, logic, etc.		* Theorems and algorithms for financial mathematics, logic, etc.

	=== Quantum information science ===

	=== Typed high-level languages for data science ===		=== Typed high-level languages for data science ===

Mechenim : /* System (software, hardware and cyber-physical) safety */

2019-03-06T21:18:15Z

System (software, hardware and cyber-physical) safety

← Version précédente		Version du 6 mars 2019 à 21:18
Ligne 7 :		Ligne 7 :
	=== System (software, hardware and cyber-physical) safety ===		=== 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.		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 ===		=== Confidentiality ===

Serwe : /* Introduction */

2019-03-04T09:10:05Z

Introduction

← Version précédente		Version du 4 mars 2019 à 09:10
Ligne 1 :		Ligne 1 :
	== Introduction ==		== 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 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.		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.

	== Societal challenges ==		== Societal challenges ==

Synthèse des prospectives 2019 - Historique des versions

Serwe : /* Confidentiality */

Serwe : /* Concepts, languages and tools for modelling and verifying complex systems */

Serwe : /* Research themes */

Serwe : /* Certified construction of systems */

Serwe : /* Certified construction of systems */

Serwe : /* Certified construction of systems */

Serwe : /* Introduction */

Mechenim le 6 mars 2019 à 21:36

Mechenim : /* System (software, hardware and cyber-physical) safety */

Serwe : /* Introduction */

Serwe : /* Confidentiality */

Serwe : /* Concepts, languages and tools for modelling and verifying complex systems */

Serwe : /* Research themes */

Serwe : /* Certified construction of systems */

Serwe : /* Certified construction of systems */

Serwe : /* Certified construction of systems */

Serwe : /* Introduction */

Mechenim : /* System (software, hardware and cyber-physical) safety */

Serwe : /* Introduction */