Engineering Interactive Systems with Model-Driven Code Contracts

The use of sound and robust software engineering techniques are essential during the design and development of safety-critical interactive systems. Failure of such systems (such as those found in medical settings or transportation) can lead to serious harm or even fatalities. Model-based development of interactive systems provides a number of benefits which can support correctness of the interface, the interaction and the functional logic of the system. Many different approaches have been proposed which target the models at different aspects of the development process (for example task analysis, interface layouts, functional behaviours etc.) and which can be used in different ways (verification of correctness, usability, testing). Typically these rely on multiple models at differing levels of abstraction. There are challenges in ensuring consistency between the models, and more importantly in ensuring that the final implementation correctly satisfies all of the models. In this paper we propose a method of deriving pre- and post-conditions for both interactive and functional elements of the system from formal models. These are used to generate code contracts within a code framework to support programmers who are implementing the system described in such models. We describe both the process for this and present an initial examination of the applicability of the approach based on a proof-of-concept user study. This small study was intended to examine whether we could correctly derive the code contracts in an automated fashion and whether or not they were usable (and beneficial) for programmers working on a pre-defined task. This initial investigation suggested that such an approach can aid programmers in correctly implementing a specification and that the general approach outlined in the paper is worth developing further.