Skip to main content
Register
Springer Professional
TOOLBAR 1 2 3 4
SEARCH
MENU 1 2 3 4
Close search form
EXTENDED SEARCH
main-content
Top
​
insite
Print
​
print
​
share

2001 | Book

Specification and Development of Interactive Systems

Focus on Streams, Interfaces, and Refinement

Introduction Read first chapter

Book Series: Monographs in Computer Science

Authors: Manfred Broy, Ketil Stølen

Publisher: Springer New York

Print ISBN: 978-1-4612-6518-4

Electronic ISBN: 978-1-4613-0091-5

Included in: Professional Book Archive

Get access Table of Contents

About this book

This book presents a fundamental mathematical and logical approach to soft­ ware and systems engineering. Considering the large number of books de­ scribing mathematical approaches to program development, it is important to explain what we consider to be the specific contribution of our book, to identify our goals, and to characterize our intended target audience. Most books dealing with the mathematics and logics of programming and system development are mainly devoted to programming in the small. This is in contrast to our book where the emphasis is on modular system development with the help of component specifications with precisely identified interfaces and refinement concepts. Our book aims at systems development carried out in a systematic way, based on a clear mathematical theory. We do not claim that this book presents a full-blown engineering method. In fact, this is certainly not a book for the application-driven software engi­ neer looking for a practical method for system development in an industrial context. It is much rather a book for the computer scientist and the scientifi­ cally interested engineer who looks for basic principles of system development and, moreover, its mathematical foundations. It is also a book for method builders interested in a proper mathematical foundation on which they can build a practical development method and industrial-strength support tools.

Table of Contents

Frontmatter

1. Introduction
Abstract
In modern technology we find interactive systems in many different forms and variations. Such systems may consist of mechanical parts, of electronic parts — called hardware, and of programs — called software. The programs are executed on the hardware. Typically, interactive systems consist of a set of components cooperating and exchanging information through interaction. In most cases, the interaction among the different components is rather sophisticated.
Manfred Broy, Ketil Stølen

2. A Guided Tour
Abstract
Our objective with this chapter is to outline and demonstrate the main specification and development techniques of Focus. The chapter is organized as a guided tour through the Focus method. We briefly explain the most central concepts and notations, we demonstrate the specification and refinement techniques, and we show that Focus Supports a classical stepwise development. Since the task of this chapter is to give a first introduction to FOCUS, the examples are simple, but nevertheless typical for interactive Systems. They all deal with the specification and implementation of unbounded buffers. An unbounded buffer is a queue that can stOre an unbounded number of data elements and return them upon request in the order they arrived.
Manfred Broy, Ketil Stølen

3. Basics
Abstract
The guided tour introduces and demonstrates the specification and refinement techniques of FOCUS. Their most significant aspects are briefly explained and illustrated by small examples. However, these explanations are not very detailed. Thus, based on the guided tour alone, it is hardly possible to gain a deep understanding of FOCUS. In the rest of this book we go through FOCUS for a second time. This time all details are carefully explained.
Manfred Broy, Ketil Stølen

4. Streams
Abstract
The central concept in FOCUS is that of a stream. Therefore, we start our detailed presentation of FOCUS with a chapter devoted to the formal definition of streams and operators for their manipulation.
Manfred Broy, Ketil Stølen

5. Specifications
Abstract
During the guided tour of Chapter 2 we demonstrated the various specification techniques of FOCUS. In particular, we distinguished between a number of frames and styles for writing specifications. Each frame and style has application areas in a system development where it is particularly suited. Any FOCUS specification can be syntactically transformed into a standard FOCUS specification describing the required behavior directly by a logical formula on timed streams. Thus, the frames and styles do not increase the expressive power of FOCUS, but help to improve the structure and readability of specifications.
Manfred Broy, Ketil Stølen

6. Examples
Abstract
The previous chapter classifies FOCUS specifications by syntactic criteria; in particular, it distinguishes among several specification frames and styles. It also introduces the basic FOCUS constructs and notations for writing specifications. In this chapter we apply the basic specification formalism of FOCUS to describe components from the following three application areas.
Manfred Broy, Ketil Stølen

7. Properties of Specifications
Abstract
In the previous two chapters we described the behavior of systems by logical properties. In this chapter we classify and structure such system properties. Classification of system properties provides valuable insights and input to systems development. First, the understanding of the system to be developed is increased. Second, different classes of properties often require specialized description and verification techniques. Third, the stepwise construction of specifications is simplified. In addition, if specifications are structured along the line of such classifications, the readability of specifications is increased and the verification of refinement steps is simplified.
Manfred Broy, Ketil Stølen

8. Equational Specification of State Transitions
Abstract
In Chapter 5 we pointed out that FOCUS supports several styles for writing elementary specifications. In this chapter, we have a closer look at one of these styles, namely, the equational style. Two other styles for elementary specifications are presented in later chapters: Chapter 10 is concerned with the graphical style, and Chapter 12 introduces the A/G style.
Manfred Broy, Ketil Stølen

9. Access Control System
Abstract
Chapter 8 introduced the equational specification style in an example-driven manner. The examples ofChapter 8 have been chosen to explain the basic principles of the equational style. They are therefore all tiny and a bit artificial. In this chapter, we apply the equational style to model an access control system (ACS). Thereby we demonstrate the suitability of the equational style in a more realistic context. A specification of the ACS first appeared in [BH93], from which we have adapted the following informal specification.
Manfred Broy, Ketil Stølen

10. Tables and Diagrams
Abstract
Readability, understandability, expressivity, and flexibility are first class goals for specification languages. The judgment as to what degree a language has these attributes depends on the background, expertise, and experiences of the persons making the judgment. In practice, presenting specifications by diagrams or tables is considered a significant help. The objective of this chapter is to show that FOCUS combines well with such more pragmatic specification and description techniques.
Manfred Broy, Ketil Stølen

11. Abracadabra Protocol
Abstract
Chapter 10 introduces state transition tables and diagrams. The emphasis is on explaining the basic principles, in particular, the relationship to purely textual Focus specifications expressed in predicate logic. The examples have been carefully selected to illustrate certain features or properties, and they are therefore both tiny and relatively trivial. The graphical specification constructs introduced in Chapter 10 can of course, in principle, also be used to describe systems of a more realistic complexity. Making the specification of nontrivial components practical requires, however, additional constructs for specification in the large, for example, hierarchical state machines in the style of Statecharts [Har87], or the SDL [ITU93] features for decomposing graphical descriptions of state machines into a number of diagrams.
Manfred Broy, Ketil Stølen

12. A/G Specifications
Abstract
In practice, system components are not designed for arbitrary environments, but only environments that satisfy certain assumptions. This motivates the introduction of so-called assumption/guarantee specifications. In fact, ever since the use of formal methods in program development became a major research area some 30 years ago, it has been common to write specifications in an assumption/guarantee style. Such specifications consist of two parts: an assumption and a guarantee. The assumption describes properties of the environment in which the specified component is supposed to run. The guarantee characterizes the constraints that the specified component is required to fulfill whenever the specified component is executed in an environment which satisfies the assumption.
Manfred Broy, Ketil Stølen

13. Memory with Locking
Abstract
Section 6.3 demonstrates the relational style for elementary specifications on several highly nondeterministic memory components. In this chapter we consider another kind of memory, namely, a shared memory with locking, and we use the A/G style to describe it. In particular, we combine the A/G style with the state transition tables and diagrams introduced in Chapter 10.
Manfred Broy, Ketil Stølen

14. Refinement
Abstract
Chapters 5 through 13 have presented all the description techniques and specification styles that are supported by FOCUS. To make proper use of this specification formalism in a system development process we need a clear understanding of what it means for a specification or a program to refine or implement another specification. In the guided tour of Chapter 2 we already touched on this matter. In this and the following three chapters, we introduce, explain, and define refinement in a much more careful manner.
Manfred Broy, Ketil Stølen

15. Behavioral Refinement
Abstract
Behavioral refinement gives a mathematical foundation to two essential system development activities, namely, stepwise requirements engineering and incremental system development. In the first case, the requirements specification is developed by adding requirements step by step in the order they are identified and formalized. In the second case, the requirements are captured, formalized, and implemented in a stepwise incremental manner. In both cases, each step typically strengthens the constraints on the system to be developed. This strengthening reduces underspecification and imposes more and more requirements. As a special case we may also refine the way the specification is formulated without changing its external behavior, for example, by introducing a glass-box view.
Manfred Broy, Ketil Stølen

16. Interface Refinement
Abstract
A specification may allow several output histories for the same input history. This is known as underspecification. Behavioral refinement is used to reduce the number of possible output histories for a given input history. Behavioral refinement does not allow output histories to be added; nor does it allow modifications to the syntactic interface. Thus, behavioral refinement characterizes what it means to reduce underspecification.
Manfred Broy, Ketil Stølen

17. Conditional Refinement
Abstract
Behavioral refinement and also interface refinement support only a rather idealistic view of system development, namely, that the final implementation behaves in accordance with the initial requirements specification for the whole spectrum of input histories. In practice, this is often unrealistic. In many cases there is a need to impose additional environment assumptions during the development. These environment assumptions are typically implementation-oriented and often not known in advance when the requirements specification is written. In other cases, they are too technical to be included in the requirements specification.
Manfred Broy, Ketil Stølen

18. Final Remarks
Abstract
Our goal with this book is to present a comprehensive formalism including specification techniques and refinement concepts for the structured and modular design and development of interactive systems, supporting timing as well as different communication and synchronization paradigms. The main emphasis is on modular abstract description of system behavior. Our approach covers many application areas including the classical tasks of software and hardware design, as well as hardware/software codesign. Nevertheless, there are many aspects of systems engineering that we have not treated. We therefore briefly relate FOCUS to some of the systems engineering paradigms used in practice today and outline some interesting research topics.
Manfred Broy, Ketil Stølen

Backmatter

Additional information

Version: 0.1215.0