Browse wiki

This paper describes the use of a domain-specific language, and an accompanying software tool, in constructing correct- by-construction control protocols for aircraft electric power systems. Given a base topology, the language consists of a set of primitives for standard specifications. The accompanying tool converts these primitives into formal specifica- tions, which are used to synthesize control protocols. We can then use TuLiP, a Python-based software toolbox, to synthesize centralized and distributed controllers. For sys- tems with no time involved in the specifications, this tool also provides an option to output specifications into a SAT-solver compatible format, thus reducing the synthesis problem to a satisfiability problem. We provide the results of our synthesis procedure on a range of topologies.