La création des systèmes cybers-physiques est une tâche complexe, ceci est d’autant plus vrai quand il s’agit de systèmes critiques. Par exemple, une erreur logicielle dans le régulateur de vitesse d’une voiture pourrait avoir des conséquences désastreuses. Ainsi, des garanties fortes d’absence d’erreurs sont requises. En plus de l’aspect humain (erreur due au développeur logiciel), un système critique doit faire face aux comportements imprévus de l’environnement avec lequel il interagit. Afin de garantir l’absence d’erreurs humaines et garantir la bonne réactivité du système, la synthèse fournit les fondements théoriques pour générer automatiquement un système correct à partir d’une spécification donnée.