摘要：This report documents the results of the Danfoss EKC trial project on model based development using IAR visualState. We present a formal state-model of a refrigeration controller based on a specification given by Danfoss. We report results on modeling, verification, simulation, and code-generation. It is found that the IAR visualState is a promising tool for this application domain, but that improvements must be done to code-generation and automatic test generation.
