This project will extend previous work in formal methods, functional languages, adaptive control and hybrid control to establish a methodology and a framework for validation and verification of adaptive/intelligent software systems. We will apply recent results in creating logical abstractions in Haskell to build a capability for automatic verification of new or modified components that meet the constraints imposed on the resulting system. If ready for use, we will apply the specification for the Open Control Platform, currently under development as part of the DARPA Software-Enabled Control project, as the definition of our distributed control platform. Our approach emphasizes the use of off-line verification and validation techniques to establish ranges of parameter variations to be allowed by the adaptive/intelligent control software and on-line techniques to ensure that approved constraints are being met. We will develop an engineering plan to demonstrate use of the Binary Decision Diagram (BDD) and Stanford Validity Checker (SVC) extensions to Haskell to automatically validate an adaptive, on-line control law redesign and implementation to meet performance specifications. This implementation will be designed to demonstrate an initial capability that can be extended to other adaptive and intelligent control systems safety critical tasks.
