Formal Development of a Safe Wheelchair Control Program

Photograph of Christoph Lüth

Christoph Lüth


In the talk, I will report about ongoing work in the SafeRobotics project, which is concerned with the formal development of a safe control program for a wheelchair for severely handicapped patients. The talk will introduce the system architecture of our wheelchair, and discuss how safety can be ensured by the formal development of a small but critical safety module. The formal development itself is done with the higher-order prover theorem prover Isabelle/HOL. First we formalise the wheelchair's kinematics in higher-order logic, and formulate a safety requirements specficiation. From this specification, we derive a design specification in the executable fragment of higher-order logic, from which we derive a second design specification using imperative features such as state and exceptions, arriving finally at an imperative program.
Tuesday 9th March 2004, 14:00
Robert Recorde Room
Department of Computer Science