A case study on reactive protocols for aircraft electric power distribution

We consider the problem of designing a control protocol for the aircraft electric power system that meets system requirements and reacts dynamically to changes in internal system states. We formalize these requirements by translating them into a temporal logic specification language describing the correct behaviors of the system, and apply formal methods to automatically synthesize a controller protocol that satisfies system properties and requirements. Through an example, we perform a design exploration to show the benefits and tradeoffs between centralized and distributed control architectures.