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