Modélisation algorithmique et synthèse d'architectures assistées par model-checking