Correct-by-Construction Design of Aircraft Electric Power Systems

by an implementation. The implementation choices are implicitly captured by a set of components, their properties, and their composition rules. A class of candidate implementations of the specication is derived by formulating and solving an optimization problem. The implementation becomes the specication for the next step in the design ow. We show how the optimization oriented formalization enables design space exploration, and we present the trade-os involved in the selection of the renement steps. We show how the methodology can be applied to the design of electric power systems by decomposing the design ow into the following steps: generator selection, generation of the connection conguration under faults, and topology design of the power distribution system.