Producing formal descriptions of low level interaction is necessary to completely capture the behaviour of user interfaces and avoid unexpected behaviour of higher level software layers. We propose a structured approach to formalising low level interaction and scaling up to higher layers, based on the composition of transducers. Every transducer encapsulates the behaviour of a device or software component, consumes and produces events. We describe transducers using a formalism based on Petri nets, and show how this transducer-based model can be used to describe simple but realistic applications and analyse unexpected defects in their design. We also identify properties that are meaningful to the application designer and users, and show how they can be formally checked on a transducer-based model of the application.
展开▼
