Towards Verifiable Adaptive Control For Safety Critical Applications

Towards Verifiable Adaptive Control for Safety Critical Applications

To be implementable in safety critical applications, adaptive controllers must be shown to behave strictly according to predetermined specifications. This thesis presents two tools for verifying specifications relevant to practical direct-adaptive control systems. The first tool is derived from an asymptotic analysis of the error dynamics of a direct adaptive controller and uncertain linear plant. The analysis yields a so called Reduced Linear Asymptotic System, which can be used for designing adaptive systems to meet transient specifications. The tool is demonstrated in two design examples from flight mechanics, and verified in numerical simulation. The second tool developed is an algorithm for direct-adaptive control of plants with magnitude saturation constraints on multiple inputs. The algorithm is a non-trivial extension of an existing technique for single input systems with saturation. Boundeness of all signals is proved for initial conditions in a compact region. In addition, the notion of a class of multi-dimensional saturation functions is introduced. The saturation compensation technique is demonstrated in numerical simulation. Finally, these tools are applied to design a direct-adaptive controller for a realistic multi-input aircraft model to accomplish control reconfiguration in the case of unforeseen failure, damage, or disturbances. A novel control design for incorporating control allocation and reconfiguration is introduced. The adaptive system is shown in numerical simulation to have favorable transient qualities and to give a stable response with input saturation constraints.

Journal of Guidance, Control, and Dynamics

Towards Verified Systems

As the complexity of embedded computer-controlled systems increases, the present industrial practice for their development gives cause for concern, especially for safety-critical applications where human lives are at stake. The use of software in such systems has increased enormously in the last decade. Formal methods, based on firm mathematical foundations, provide one means to help with reducing the risk of introducing errors during specification and development. There is currently much interest in both academic and industrial circles concerning the issues involved, but the techniques still need further investigation and promulgation to make their widespread use a reality.This book presents results of research into techniques to aid the formal verification of mixed hardware/software systems. Aspects of system specification and verification from requirements down to the underlying hardware are addressed, with particular regard to real-time issues. The work presented is largely based around the Occam programming language and Transputer microprocessor paradigm. The HOL theorem prover, based on higher order logic, has mainly been used in the application of machine-checked proofs.The book describes research work undertaken on the collaborative UK DTI/SERC-funded Information Engineering Dictorate Safemos project. The partners were Inmos Ltd., Cambridge SRI, the Oxford University Computing Laboratory and the University of Cambridge Computer Laboratory, who investigated the problems of formally verifying embedded systems. The most important results of the project are presented in the form of a series of interrelated chapters by project members and associated personnel. In addition, overviews of two other ventures with similar objectives are included as appendices.The material in this book is intended for computing science researchers and advanced industrial practitioners interested in the application of formal methods to real-time safety-critical systems at all levels of abstraction from requirements to hardware. In addition, material of a more general nature is presented, which may be of interest to managers in charge of projects applying formal methods, especially for safety-critical-systems, and others who are considering their use.