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

fYear

1999

fDate

36434

Firstpage

267

Lastpage

270

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 1999. 14th IEEE International Conference on.

Conference_Location

Cocoa Beach, FL

Print_ISBN

0-7695-0415-9

Type

conf

DOI

10.1109/ASE.1999.802313

Filename

802313