Case Studies
Focus on Isabelle
LaTeX representation

The FOCUS framework is developed at Technische Universität München (chair of Prof. Manfred Broy) for the formal specification and stepwise development of distributed systems. This methodology offers a variety of well-tuned formalisms, different guidelines for the systematic system development as well as a sophisticated refinement concept. The development process of FOCUS is based on modeling systems as networks of components communicating asynchronously via unbounded, directed channels.

Thus, a distributed system in FOCUS is represented by components connected by communication links called channels. Components are systems that are described in terms of their (input/output) behavior which is total. The components may interact or work independently from one another. The channels in this specification framework are asynchronous communication links without delays. They are directed, reliable, and order preserving. Via these channels components exchange information in terms of type messages. Messages are passed along the channels one after the other and delivered in exactly the same order in which they were sent.

An interface specification is characterized through the relation between communication histories for the external input and output channels. External considering the distinction between component interface and component internal specification (which might also have internal channels). The formal meaning of a specification is exactly this external input/output relation.

The main concept in Focus is the stream. Streams represent the communication histories of directed channels. They are formally represented by functions mapping the indexes in their time domains to their messages.

In this framework we treat both elementary and composite specifications. Elementary specifications are the building blocks for system representation. In any case we distinguish among three frames: the untimed, the timed and the time-synchronous frame.

Based on the FOCUS Theory a tool suite exists, called AutoFocus, that gives engineering support for applying the method.

On this webpage you can find a number ob publications about FOCUS as well as about a number of case studies of modelling in FOCUS, short discriptions of the case studies and the projects that uses the framework, an introduction to a package to represent FOCUS specifications in LaTeX, and the AutoFocus CASE tool for the development of distributed systems that is based on the FOCUS methodology. We also present here a specification and verification methodology Focus on Isabelle that is a coupling of FOCUS with an interactive verification system Isabelle/HOL.

               focus logo

  Maria Spichkova
  Last modified 20.07.2011