Résumé
Formal methods can strongly contribute to improve dependability of logic controllers during design, by providing means to avoid flaws due to designers' omissions or specifications misinterpretations. This communication presents a formal synthesis method whose goal is to obtain the control laws of a logic system from specifications given in natural language. The formal framework underlying the method is the Boolean algebra of n-variable switching functions. The operations and relations of this algebra enable to represent controller specifications formally, to detect inconsistencies within specifications and to generate control laws with optimization criteria. The application of this formal design method to an example permits to illustrate its main advantages.