A Caltech Library Service

Formal Synthesis of Embedded Control Software: Application to Vehicle Management Systems

Wongpiromsarn, T. and Topcu, U. and Murray, R. M. (2011) Formal Synthesis of Embedded Control Software: Application to Vehicle Management Systems. In: Infotech@Aerospace 2011. AIAA , Reston, VA, Art. No. 2011-1506. ISBN 9781600869440.

[img] PDF - Published Version
See Usage Policy.


Use this Persistent URL to link to this item:


Motivated by the transition from federated to integrated architectures in aerial vehicles, we propose an automated methodology for the synthesis of correct-by-construction control protocols for vehicle management systems. We use linear temporal logic as the specification language for precisely describing correct behaviors of the system as well as the admissible dynamic behavior of the environment due to, for example, wind gusts and changes in the flight conditions. We apply the method in the context of dynamic power allocation among a number of subsystems of varying flight-criticality. The resulting power management protocol is guaranteed to be correct, with respect to the overall system specification, for all admissible environment profiles. This approach also enables reasoning about design tradeoffs such as between efficiency (imposed through formal specifications) and system weight (characterized by the amount of required power generation and energy storage). We present our preliminary results in a simple setting and discuss extensions of the methodology to capture more realistic system and environment models and specifications.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Murray, R. M.0000-0002-5785-7481
Additional Information:© 2011 American Institute of Aeronautics and Astronautics. The authors gratefully acknowledge Michel Ingham, Scott Livingston, Necmiye Ozay and Mumu Xu and for the helpful discussions and comments on the paper. This work is partially supported by AFOSR and the Boeing Corporation.
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)UNSPECIFIED
Boeing CorporationUNSPECIFIED
Other Numbering System:
Other Numbering System NameOther Numbering System ID
AIAA Paper2011-1506
Record Number:CaltechAUTHORS:20190930-110459012
Persistent URL:
Official Citation:Formal Synthesis of Embedded Control Software: Application to Vehicle Management Systems Tichakorn Wongpiromsarn, Ufuk Topcu, and Richard Murray Infotech@Aerospace 2011.
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:98943
Deposited By: George Porter
Deposited On:30 Sep 2019 20:12
Last Modified:03 Oct 2019 21:45

Repository Staff Only: item control page