(Bremen)

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.Robert Recorde Room

Department of Computer Science