System-level automatic model refinement

In a system-level design methodology, the system under design is represented by design models with different levels of abstraction. The design process is essentially a series of steps that gradually transform the most abstract specification model into a detailed implementation model. In practice, the designers spend long time to manually write these design models. In addition, it is not possible to verify the equivalence between the models written manually. In this dissertation I present my work on automatic model refinement, 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 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. I approach the problem by first formally defining the semantics and styles of the input specification model and the output architecture model. By looking at the differences between the two models, a series of transformations can be defined to refine the specification model into the architecture model.;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 refinement.