Component-Based Synthesis of Embedded Systems Using Satisfiability Modulo Theories
Component-Based Synthesis of Embedded Systems Using Satisfiability Modulo Theories
复制标题
使用可满足性模理论进行基于组件的嵌入式系统综合
DOI：
10.1145/2746235
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
T. Givargis
中科院分区：
文献类型：
--
作者：
Steffen Peter;T. Givargis
约束编程求解器，例如可满足性模理论(SMT)求解器，是从大的设计空间中为嵌入式系统寻找更好的配置的有效工具。然而，构建SMT约束程序并不是一件容易的事情，特别是对于表现出多个视点和模型的复杂系统。在本文中，我们提出了Codel：一种基于组件的描述语言，它允许系统设计人员将组件表达为系统的可重用构建块，以及它们的可参数化属性、模型和互连。系统是通过分配、连接和参数化组件来合成的，以满足应用程序的需求。我们提出了一种算法，将可用代码表示的基于组件的设计空间转换为SMT程序，该程序由最先进的SMT求解器求解，确定综合问题的可满足性，并提供按构造正确的系统配置。对分布式实时进程调度和映射领域用例的评估结果证实了SMT相对于传统设计空间探索方法的性能提升，通过用代码表达设计问题的可用性提升，以及Codel/SMT方法支持嵌入式系统设计的能力。
Constraint programming solvers, such as Satisfiability Modulo Theory (SMT) solvers, are capable tools in finding preferable configurations for embedded systems from large design spaces. However, constructing SMT constraint programs is not trivial, in particular for complex systems that exhibit multiple viewpoints and models. In thisarticle we propose CoDeL: a component-based description language that allows system designers to express components as reusable building blocks of the system with their parameterizable properties, models, and interconnectivity. Systems are synthesized by allocating, connecting, and parameterizing the components to satisfy the requirements of an application. We present an algorithm that transforms component-based design spaces, expressible in CoDeL, to an SMT program, which, solved by state-of-the-art SMT solvers, determines the satisfiability of the synthesis problem, and delivers a correct-by-construction system configuration. Evaluation results for use cases in the domain of scheduling and mapping of distributed real-time processes confirm, first, the performance gain of SMT compared to traditional design space exploration approaches, second, the usability gains by expressing design problems in CoDeL, and third, the capability of the CoDeL/SMT approach to support the design of embedded systems.