Assumption/Commitment Rules for Data-flow Networks with an Emphasis on Completeness

During the last 15 years a large number of specification techniques based on the so-called assumption/commitment paradigm have been proposed. The formulation of verification rules for the composition of such specifications is known to be a difficult task. Most rules published so far impose strong constraints on the type of properties that can be expressed by the assumptions. Moreover, if completeness results are provided at all they are normally quite weak. We investigate these problems in the context of a model for data-flow networks.     «

During the last 15 years a large number of specification techniques based on the so-called assumption/commitment paradigm have been proposed. The formulation of verification rules for the composition of such specifications is known to be a difficult task. Most rules published so far impose strong constraints on the type of properties that can be expressed by the assumptions. Moreover, if completeness results are provided at all they are normally quite weak. We investigate these problems in the c...     »