next up previous contents
Next: Scientific Output from Up: Scientific Output from Previous: Scientific Output from

Relevant Papers

 

[Fuchs, Philipps 95]
M Fuchs and J Philipps, Formal Development of a Production Cell in Focus --- A Case Study, in Formal Development of Reactive Systems: Case Study Production Cell, Claus Lewerentz, Thomas Linder (editors), Lecture Notes in Computer Science 891, pages 187 -- 200, 1995

A specification for a production cell is developed using the design method Focus. The specification comprises both the components and the corresponding control programs. This work investigates the suitability of a rule system for the stepwise refinement of distributed systems in an assumption/commitment style. As a running example we consider the elevating rotary table of a production cell. Besides descriptive and constructive specifications for this component an executable simulation program in a functional language is presented.

[Fuchs 94]
M Fuchs, Technologieabhaengigkeit von Spezifikationen digitaler Hardware, PhD-Thesis, Technische Universitaet Munchen, SFB-Bericht 342/14/94 A, 1994

This work covers the aspect of technology dependency in specifications of digital hardware at the register transfer level. As running examples we choose the RS-flipflop and bus structures. The technologies are NMOS and CMOS. For the RS-flipflop and the bus structures technology independent and technology dependent specifications are given and related by an adequate refinement relation. It turns out that in general specifications at the register transfer level are not technology independent.

[Fuchs, Stølen]
M Fuchs and K Stølen, Development of a Distributed Min/Max Component, in Proceedings of the 3. GI-Workshop on ``Anwendungen formaler Methoden beim Entwurf von Hardwaresystemen'', W. Grass and M. Mutz (editors), 1995, Passau, also appeared as SFB-Bericht 342/18/93 A.

We introduce a specification technique and a refinement calculus for networks of components communicating asynchronously via unbounded FIFO channels. Specifications are formulated in a relational style. The given refinement rules allow modular system development in a step-wise, top-down manner. We employ the proposed formalism to specify and develop a so-called Min/Max Component. First an overview of the whole design process is given. Then certain steps of the development are described in detail.

[Fuchs, Mendler 95]
M Fuchs and M Mendler, Functional Semantics for Delta-Delay VHDL based on Focus, in Formal Semantics for VHDL, C. Delgado Kloos and P. Breuer (editors), Kluwer Academic Publishers, pages 9 -- 42, ISBN 0-7923-9552-2, 1995

This tutorial paper gives a functional semantics for delta-delay VHDL, i.e. VHDL restricted to zero-delay signal assignments. In combination with the sequential statements zero-delay signal assignment is sufficient to generate the full algorithmic expressibility of VHDL. The restriction is useful for a formal semantics of VHDL aimed at higher levels of abstraction where real, absolute, and precise timing often is painful if not impossible to prescribe. The approach employs the functional specification methodology Focus which is based on the concept of streams and stream-processing functions. It advocates a three-level semantics reflecting VHDL's three syntactic levels of expressions, statements, and processes.

[Broy 95]
M Broy, Advanced Component Interface Specification, in Takayasu Ito, Akinori Yonezawa (Eds.), Theory and Practice of Parallel Programming, International Workshop TPPP'94, Sendai, Japan, November 7 -- 9, 1994, Proceedings, Lecture Notes in Computer Science 907, Springer 1995

We introduce a method for the specification of reactive asynchronous components with a concurrent access interface and outline its mathematical foundation. The method supports the specification of components that show a complex reactive behavior including timing aspects. Examples are the non-strict fair merge or the arbiter. The method supports the specification of reactive systems and their modular composition into data flow networks. The specification approach is compositional. It supports the integrated specification and verification of both safety and liveness conditions in modular system descriptions. We outline particular specification styles that may be useful for the better readability of such specifications.



next up previous contents
Next: Scientific Output from Up: Scientific Output from Previous: Scientific Output from



Bernhard Moeller
Fri May 12 14:21:20 MET DST 1995