Compositional Comparison of Formal Software Specifications Using Transformation Systems |
| |
Authors: | Martin Große-Rhode |
| |
Affiliation: | Technische Universit?t Berlin, Berlin, Germany, DE
|
| |
Abstract: | In a model-based software systems development formal specifications of the components of the system are developed. Thereby
different specifications are used to represent the different aspects or views of the components, possibly following different
paradigms. These heterogeneous viewpoint specifications have to be integrated in order to obtain a consistent global specification
of the whole system. In this paper transformation systems are introduced as a common semantic domain where specifications
written in different languages can be interpreted and formally compared. A transformation system is a transition system where
the transitions are labelled by sets of actions and the states are labelled by algebras representing the data states. Development
relations and composition operations for transformation systems are investigated, and it is shown that compatible local developments
of components induce a global development of their composition. As an application two specifications of the alternating bit
protocol are formally compared component-wise, one given in the process calculus CCS, the other one in the parallel programming
language UNITY.
Received September 2000 / Accepted in revised form June 2001 |
| |
Keywords: | : Compositionality Consistency Formal specification Integration |
本文献已被 SpringerLink 等数据库收录! |
|