Constraints Assisted Modeling and Validation in Metropolis Framework

This paper focuses on quantitative constraints specified with logic of constraints (LOC) and coordination constraints with linear temporal logic (LTL) that are used in the specification, modeling, and validation of heterogeneous embedded system design. Quantity annotation is the principal approach for modeling performance information in Metropolis, our experiment platform. Quantitative constraints are then used to enforce and to refine simulation. They can also be used in synthesis settings especially for deciding system level parameters such as scheduling and hardware-software partitioning. Similarly, we utilize LTL in Metropolis to quickly refine the system behavior especially process coordinations. On the validation aspect, LOC and LTL are also used to specify assertions for simulation and for formal verification. We demonstrate our approach with a multimedia example from the industry.