A Contract-Based Methodology for Aircraft ElectricPower System Design

Author(s): Pierluigi Nuzzo, Mumu Xu, Necmiye Ozay,John B. Finn, Alberto Sangiovanni-Vincentelliand Richard Murray, Alexandre Donze, SanjitSeshia

Citation
Pierluigi Nuzzo, Mumu Xu, Necmiye Ozay,John B. Finn, Alberto Sangiovanni-Vincentelliand Richard Murray, Alexandre Donze, SanjitSeshia. "A Contract-Based Methodology for Aircraft ElectricPower System Design". IEEE Access, November 2014.

Abstract
In an aircraft electric power system, one or moresupervisory control units actuate a set ofelectromechanical switches to dynamicallydistribute power from generators to loads, whilesatisfying safety, reliability, and real-timeperformance requirements. To reduce expensiveredesign steps, this control problem is generallyaddressed by minor incremental changes on top ofconsolidated solutions. A more systematic approachis hindered by a lack of rigorous designmethodologies that allow estimating the impact ofearlier design decisions on the finalimplementation. To achieve an optimalimplementation that satisfies a set ofrequirements, we propose a platform-basedmethodology for electric power system design,which enables independent implementation of systemtopology (i.e., interconnection among elements)and control protocol by using a compositionalapproach. In our flow, design space exploration iscarried out as a sequence of refinement steps fromthe initial specification toward a finalimplementation by mapping higher level behavioraland performance models into a set of eitherexisting or virtual library components at thelower level of abstraction. Specifications arefirst expressed using the formalisms of lineartemporal logic, signal temporal logic, andarithmetic constraints on Boolean variables. Toreason about different requirements, we usespecialized analysis and synthesis frameworks andformulate assume guarantee contracts at thearticulation points in the design flow. We showthe effectiveness of our approach on aproof-of-concept electric power system design.

---

Citation Formats

• HTML
  

                  
  Pierluigi Nuzzo, Mumu Xu, Necmiye Ozay,John B. Finn, Alberto Sangiovanni-Vincentelliand Richard Murray, Alexandre Donze, SanjitSeshia.
  "<a href="https://www.icyphy.org/publications/2014_NuzzoEtAl/">A Contract-Based Methodology for Aircraft ElectricPower System Design</a>".
  <i>IEEE Access</i>, November 2014.
                  
                  

• Plain Text
  

                  
  Pierluigi Nuzzo, Mumu Xu, Necmiye Ozay,John B. Finn, Alberto Sangiovanni-Vincentelliand Richard Murray, Alexandre Donze, SanjitSeshia.
  "A Contract-Based Methodology for Aircraft ElectricPower System Design".
  IEEE Access, November 2014.
                  
                  

• BibTeX
  

                      
  @article{NuzzoXuOzayFinnSangiovanniVincentelliMurrayDonzeSeshia14_ContractBasedMethodologyForAircraftElectricPowerSystem,
  	author = {Pierluigi Nuzzo, Mumu Xu, Necmiye Ozay,John B. Finn, Alberto Sangiovanni-Vincentelliand Richard Murray, Alexandre Donze, SanjitSeshia},
  	title = {A Contract-Based Methodology for Aircraft ElectricPower System Design},
  	journal = {IEEE Access},
  	month = {November},
  	year = {2014},
  	abstract = {In an aircraft electric power system, one or moresupervisory control units actuate a set ofelectromechanical switches to dynamicallydistribute power from generators to loads, whilesatisfying safety, reliability, and real-timeperformance requirements. To reduce expensiveredesign steps, this control problem is generallyaddressed by minor incremental changes on top ofconsolidated solutions. A more systematic approachis hindered by a lack of rigorous designmethodologies that allow estimating the impact ofearlier design decisions on the finalimplementation. To achieve an optimalimplementation that satisfies a set ofrequirements, we propose a platform-basedmethodology for electric power system design,which enables independent implementation of systemtopology (i.e., interconnection among elements)and control protocol by using a compositionalapproach. In our flow, design space exploration iscarried out as a sequence of refinement steps fromthe initial specification toward a finalimplementation by mapping higher level behavioraland performance models into a set of eitherexisting or virtual library components at thelower level of abstraction. Specifications arefirst expressed using the formalisms of lineartemporal logic, signal temporal logic, andarithmetic constraints on Boolean variables. Toreason about different requirements, we usespecialized analysis and synthesis frameworks andformulate assume guarantee contracts at thearticulation points in the design flow. We showthe effectiveness of our approach on aproof-of-concept electric power system design.},
  	URL = {https://www.icyphy.org/publications/2014_NuzzoEtAl/}
  }