摘要:

Interaction objects (interactors) are abstract structures that provide a link between rigorous approaches to software development and user-oriented aspects of interaction. The focus of the paper is on the second role of interactors; in particular, how a formal model of interaction can be used to classify and clarify various properties of interactive behaviour that are important from a user-oriented viewpoint. The formal model used in this discussion abstracts away from distinctions between states, events, and renderings; when needed, these concepts are introduced as various projections on the basic model.

DOI:10.1049/sej.1995.0002

出版商:IEE    

年代:1995

数据来源: IET

摘要:

The trend towards systems that support a rich variety of interaction techniques has consequences for the traditional understanding of software design practice. Formal approaches to software development have mainly focused on design expressions that avoid explicit discussion of interactive behaviour. The emphasis in rigorous development is on transforming a mathematical specification into an implementation through a series of valid refinement steps. However, any design process for interactive systems must also add user oriented requirements. It is suggested that a suitable concern for human factors can be folded into a rigorous development process by generalising from functional models and refinement to models that provide multiple viewpoints onto the design artefacts. The paper provides an overview of the relevant perspectives and describes work aimed at integrating them within the specification phase of software development.

DOI:10.1049/sej.1995.0003

出版商:IEE    

年代:1995

数据来源: IET

摘要:

Temporal logic techniques have been proposed as a way of achieving a very natural transition from informal requirements to a formal specification of the requirements. The paper presents a case study of a real-life system developed using such techniques. Both a top-level specification and implementation semantics are given in temporal logic. In particular, the progression from statements in English to temporal logic is highlighted. A correctness proof that the implemented system satisfies the specification has been produced.

DOI:10.1049/sej.1995.0004

出版商:IEE    

年代:1995

数据来源: IET