Démonstration de la sécurité d'une application de signalisation en mode nominal et en modes dégradés par la preuve formelle Chapter