Subproject A6
 
 
 

Survey
Research
Cooperations
Literature
People
Links
Contact
    SFB 342A The Sonderforschungsbereich SFB 342 Tour


    Subproject A6

    Distributed Systems Design Methodology

    Research Topics

    The main contribution of subproject A6 is the development of FOCUS, a formal methodology for the specification and stepwise development of distributed, reactive systems. AutoFocus, a tool prototype based on the FOCUS concepts, is designed to support the practical usability of the methodology. 

    FOCUS and AutoFOCUS are described in brief in the following sections.

    FOCUS - A Design Methodology for Distributed Systems

    FOCUS supplies a methodology for the formal specification and the stepwise development of distributed systems. In this framework systems are modeled by networks of components communicating asynchronously via unbounded, directed channels.

    The system development process consists of several phases of abstraction:

    • During the Requirement Phase a first formalization of an informal description is developed. It will be used as the basis for the following phases. In this step specifications can be formalized as either trace or functional specifications. The transition between these paradigms is formally sound and preserving correctness.
    • During the Design Phase the essential part of the system development is carried out by developing the structure of the systems and refining it up to the intended level of granularity. Here, the specifications are based on one denotational semantics which models specifications by sets of stream processing functions. Each function describes a possible acceptable behavior. For the development of the specifications during the design phase paradigms like functional and relational specifications as well as several specification styles like Assumption/Commitment or equational specifications are supplied. Due to the specific natures of these variants they can be used tailor-made for the solution of specific problems. 
    • During the Implementation Phase the specification which was developed during the design phase is transformed into one of the supplied goal languages.
    To increase its usability FOCUS is adapted for the use of engineering oriented and practically used techniques and formalisms like tables, diagrams or state-charts.

    During the formal development of distributed systems the intended level of granularity is reached by stepwise refinement of the system. For this purpose FOCUS offers a powerful compositional refinement concept as well as refinement calculi. Examples for those refinement concepts are:

    Behavioral Refinement: 
    The aim of this refinement is the elimination of underspecification as it is needed e.g. for the specification of fault-tolerant behavior. On the semantic level this refinement is modeled by set inclusion.
    Interface Refinement: 
    Here, the interface of a specification is refined by changing the number or types of the channels.
    Structural Refinement: 
    This concept allows the development of the structure of the distributed system by refining components by networks of components.

     

     

    On the whole FOCUS offers a mathematically and conceptually sound framework allowing a complete system development from an abstract requirement specification to the implementation. 

    The AutoFocus Tool

    The AutoFocus tool prototype supports the development of distributed systems using industrial oriented, mostly graphical description techniques based on the formal methodology FOCUS. The supported description techniques are:
    • System diagrams to describe the system strucuture, 
    • Data types to described message types for channels or local data of system components, 
    • Automata to specify the behaviour of the components,
    • Message Sequence Charts to describe (exemplary) system runs. 
    A detailed description of AutoFocus can be found on the AutoFocus web-page as well as in an introductory article.

    Planned Research Topics

    The planned research topics include the methodical extension of the FOCUS approach up to a general development model and thus the integration of additional description techniques of industrial character. Additionally, an improvement of the proof support is planned, incorporating application oriented description techniques as far as possible. Furthermore, a methodical support for proof development is considered. Consequently, AutoFocus will be enhanced with an interface to interactive and automatic theorem provers. To complete this orientation towards applicability, concrete methods for specific application areas are planned, as, for example, multi-media broadband networks, analysis of security aspects, or operating systems (in joint work with subproject A8).

    Max Breitling, Bernhard Schätz, Katharina Spies, Sept. 1997 
Max Breitling,

Bernhard Schätz,
Sept. 1997