Theory of interactions and scenes for user centered systems specification and verification

Scenario-based design is a significant informal approach to systems specification and verification, but it does not ensure correct user-centered systems. This paper shows how scenario-based design can be augmented with a theory of interactions and scenes that allows the designer to elicit user requirements within a formal framework that does not constrain excessively the user narration, and to derive a system implementation satisfying the basic software engineering requisites. The paper discusses also how the approach facilitates the formal proof of the safety and liveness properties of interactive systems.