View source for SURF 2015: Formal synthesis of switching protocols for estimation and control of aircraft electric power systems

'''[[SURF 2015|2015 SURF]] project description'''
* Mentor: Richard M. Murray
* Co-mentors: Benson Christalin and Scott C. Livingston

[[File:Testbed-photograph-20141222-0833.jpg|400px|thumb|Figure 1. The test bed as of 22 Dec 2014.  The relay board is green and toward the right side of the photograph.  While not shown here, it attaches to a computer via USB to allow control from software.]]

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 [http://tulip-control.org 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 [http://ptolemy.eecs.berkeley.edu/ Ptolemy II] to use [https://www.fmi-standard.org/ FMI].

For additional context, consult relevant SURF descriptions from [https://www.cds.caltech.edu/~murray/wiki/index.php/SURF_2014:_Switching_control_synthesis_in_the_presence_of_uncertainty_and_general_loads_for_an_aircraft_electric_power_system_testbed 2014] and [https://www.cds.caltech.edu/~murray/wiki/index.php/SURF_2012:_Aircraft_electric_power_system_modeling_in_SIMULINK/Stateflow 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; [[http://dx.doi.org/10.1109/ACCESS.2013.2295764 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; [[http://dx.doi.org/10.1145/2461328.2461344 DOI]][[http://resolver.caltech.edu/CaltechAUTHORS:20130115-094546873 tech report]].

[3] L. Persson, S.C. Livingston, and R.M. Murray. An improved aircraft electric power testbed for validating synthesis methods.  <i>submitted</i> for the [http://nasaformalmethods.org/ NASA Formal Methods Symposium]. Nov 2014; [[http://scottman.net/pre/plm_nfm15_submitted.pdf 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; [[http://www.cds.caltech.edu/~murray/papers/2013b_mxom13-cdc.html preprint]].

[5] R. G. Michalko, ``Electrical starting, generation, conversion and distribution system architecture for a more electric vehicle,'' [http://patft.uspto.gov/netacgi/nph-Parser?patentnumber=7439634 U.S. Patent 7 439 634], Oct. 21, 2008.