SURF 2015: Formal synthesis of switching protocols for estimation and control of aircraft electric power systems
2015 SURF project description
- Mentor: Richard M. Murray
- Co-mentors: Benson Christalin and Scott C. Livingston
The electric power system (EPS) has come to be a large and crucial part of modern aircraft. Designs include a variety of power sources---from AC generators to DC batteries---and several types of load buses with different criticality levels [5]. Electric power is typically routed throughout the aircraft using a network of contactors. Each contactor can be commanded to be closed or open, effectively connecting or disconnecting the corresponding circuit branch. The control problem in this context is to find a switching protocol for contactor configurations so as to guarantee formally specified properties, often referred to as "the requirements." For example, it is unsafe to attach two AC generators in parallel, and thus it is a requirement that contactor configurations in which that occurs are always avoided.
Such complicated designs are challenging for traditional engineering practices and motivate the introduction of formal verification and synthesis methods [1]. Since experiments on an actual aircraft EPS are not yet feasible, we have developed a small test bed for validating implementations from our research on fault detection and correct-by-construction control [2], [3], [4]. http://vimeo.com/112469771 displays a demo of the implementation of fault detection on the test bed on Aug 2014. Figure 1 is a recent photograph.
An important direction of future work is exploring control in the midst of sensing. This refers broadly to the need to estimate changes to the states of components in an EPS while controlling contactors so as to maintain safety. Continuing with the earlier example requirement, the controller must not parallel two generators while it is experimentally switching contactors to localize a wiring failure. The practical motivation is built-in test (BIT), which are automatic procedures that use internal logic and hardware to characterize the quality, performance and reliability of the system, both before and during flight. During the SURF, the student would make use of and possibly contribute new code to the Temporal Logic Planning (TuLiP) toolbox.
There are also improvements that can be made to the test bed, which the SURF can involve according to desires of the student. E.g.,
- expanding the test bed to model new types of faults;
- improving modularity to ease addition of new components;
- extending the current model in Ptolemy II to use FMI.
For additional context, consult relevant SURF descriptions from 2014 and 2012.
References
[1] P. Nuzzo, H. Xu, N. Ozay, J.B. Finn, A.L. Sangiovanni-Vincentelli, R.M. Murray, A. Donzé, and S.A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2: 1--25. Jan 2014; [DOI].
[2] R. Rogersten, H. Xu, N. Ozay, U. Topcu, and R.M. Murray. An Aircraft Electric Power Testbed for Validating Automatically Synthesized Reactive Control Protocols. in Proceedings of HSCC, pp. 89--94. Apr 2013; [DOI][tech report].
[3] L. Persson, S.C. Livingston, and R.M. Murray. An improved aircraft electric power testbed for validating synthesis methods. submitted for the NASA Formal Methods Symposium. Nov 2014; [draft (under review)].
[4] Q. Maillet, H. Xu, N. Ozay, and R.M. Murray. Dynamic State Estimation in Distributed Aircraft Electric Control Systems via Adaptive Submodularity. in Proceedings of CDC. Dec 2013; [preprint].
[5] R. G. Michalko, "Electrical starting, generation, conversion and distribution system architecture for a more electric vehicle," U.S. Patent 7 439 634, Oct. 21, 2008.
