Title :
Development of a constraint-based airlift scheduler by program synthesis from formal specifications
Author :
Emerson, Thomas ; Burstein, Mark H.
Author_Institution :
Kestrel Inst., Palo Alto, CA, USA
Abstract :
We describe the formal specification and automated synthesis of a strategic airlift scheduler for the Air Mobility Command of the US Air Force. The program synthesis system, the Kestrel Interactive Development System, composes a formal domain theory with a formal description of a class of algorithms (global search with constraint propagation) to produce provably correct and highly efficient code that outperforms more conventional approaches to this scheduling problem
Keywords :
aircraft; automatic programming; command and control systems; constraint handling; formal specification; interactive systems; scheduling; Air Mobility Command; Kestrel Interactive Development System; US Air Force; automated synthesis; constraint based airlift scheduler; constraint propagation; formal description; formal domain theory; formal specifications; global search; highly efficient code; program synthesis system; provably correct; scheduling problem; strategic airlift scheduler; Aircraft propulsion; Airports; Constraint optimization; Control system synthesis; Databases; Formal specifications; Identity-based encryption; Large-scale systems; Monitoring; Scheduling;
Conference_Titel :
Automated Software Engineering, 1999. 14th IEEE International Conference on.
Conference_Location :
Cocoa Beach, FL
Print_ISBN :
0-7695-0415-9
DOI :
10.1109/ASE.1999.802313
