A Formal Model for Embedded Brain Reading
Elsa Andrea Kirchner, Rolf Drechsler
In Industrial Robot: an International Journal, Emerald Group Publishing Limited, volume 40, number 6, pages 530-540, 2013.
The presented work contributes to research in the field of advanced man-machine interaction and to research in the field of formalisation and verification of complex systems. The paper describes for the first time embedded brain reading (eBR) and presents a formal model for it. It illustrates how an error-prone approach like brain reading (BR) can be applied safely by embedding it into the control of a real system and by applying mechanisms that control for its correct function. This work was motivated by the need to provide a detailed and well understandable formal description of eBR. We first introduce eBR and point out its main features. Next a general model for eBR is developed to describe the overall architecture, integral parts and dependencies between those parts. The model is developed and presented in a formal structured form that allows for application of optimisation as well as verification techniques. We demonstrate using implementations that the application of the formal model allows to check for completeness and correct- ness to detect errors in implementations, which were invisible without formalising eBR. In summary, the presented work contributes a formal model for a complex system and shows that such a formal model can improve the overall systems functionality. For future work our results support the application of formal modelling and verification techniques at the system level and the development of methods to prove for correctness and completeness of complex systems during their development.