|
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.
| 
