A tool-supported design framework for safety critical interactive systems

Abstract

This paper presents a design framework for safety critical interactive systems, based on a formal description technique called the ICO (Interactive Cooperative Object) formalism. ICO allows for describing, in a formal way, all the components of highly interactive (also called post-WIMP) applications. The framework is supported by a case tool called PetShop allowing for editing, verifying and executing the formal models. The first section describes why such user interfaces are challenging for most description techniques, as well as the state of the art in this field. Section 3 presents a development process dedicated to the framework. Then, we use a case study in order to recall the basic concepts of the ICO formalism and the recent extensions added in order to take into account post-WIMP interfaces' specificities. Section 5 presents the case tool PetShop and how the case study presented in the previous section has been dealt with. Lastly, we show how PetShop can be used for interactive prototyping.