In the first part of this talk I′ll introduce control engineering as a new domain of application for formal methods. I′ll discuss design verification, drawing attention to the role played by diagrammatic evaluation criteria involving numeric plots of a design, such as Nichols and Bode plots. I′ll show that symbolic computation and computational logic can be used to discharge these criteria and provide symbolic, automated, and very general alternatives to these standard numeric tests, and illustrate our work with reference to a standard reference model drawn from military avionics.<br>At the heart of this work is the observation that control systems based on linear differential equations exhibit ″program–like″ phenomena such as loops and sequential composition, which allows the development of a Hoare–style logic. While trying to understand this phenomenon we hit upon a new abstract presentation of Hoare Logic based on categories with feedback, which can also be used to capture extensions of the standard Hoare logic for while programs, e.g. the extension with pointer manipulations via separation logic. <b>Keywords:</b>
Abbrevation
BCS-FACS
City
London
Country
UK
Start Date
End Date
Abstract