A graph rewriting approach for transformational design of digitalsystems

摘要

Transformational design integrates design and verification. Itcombines “correctness by construction” and design creativityby the use of pre-proven behaviour preserving transformations as designsteps. The formal aspects of this methodology are hidden in thetransformations. A constraint is the availability of a designrepresentation with a compositional formal semantics. Graphrepresentations are useful design representations because of theirvisualisation of design information. In this paper graph rewritingtheory, as developed in the last twenty years in mathematics, is shownto be a useful basis for a formal framework for transformational design.The semantic aspects of graphs which are no part of graph rewritingtheory are included by the use of attributed graphs. The used attributealgebra, table algebra, is a relation algebra derived from databasetheory. The combination of graph rewriting, table algebra andtransformational design is new