by Junyu Peng
In a system-level design methodology, the system under design is represented by models at different abstraction levels. The design process is essentially a series of steps that gradually transform the most abstract specification model into a detailed implementation model. In practice, all these models are written manually by designers. As the result, the designers spend long time on this tedious and error-prone model-writing task. In addition, it is not possible to verify the equivalence between the models written manually. In this dissertation we present our work on automatic model generation, where models are generated automatically by tools rather than manually by designers. This kind of automation not only relieves designers from the mundane and time-consuming coding task but also makes it possible to formally verify the functional equivalence between models.
This dissertation in particular focuses on the architecture refinement, which is aimed to automatically generate an architecture model from the input specification model after architecture exploration when architecture allocation and partitioning decisions are made. We approach the problem by first formally defining the semantics and styles of the input specification model and the output architecture model. Based on the differences between the input and output models, we are able to define a refinement flow which consist of a series of formally-defined transformations.
Distinguishing itself from other similar approaches, our approach addresses the quality issue of the automatically generated models. We defined a set of quality metrics that are relevant to architecture refinement. Then we devised several optimization algorithms which can be embedded into the transformations to improve the quality of the output model.
In order to prove the feasibility of our approach, we implemented an automatic model refinement engine which is targeted at the SpecC language. We validated the effectiveness of our approach by applying the refinement engine to a couple of large, real-life applications. Experimental results demonstrate that 1000x productivity gain is achievable with automatic model generation.