Improving platform-based system synthesis by satisfiability modulo theories solving

Due to the ever increasing system complexity, deciding whether a given platform is sufficient to implement a set of applications under given constraints becomes a serious bottleneck in platform-based design. As a remedy, the work at hand proposes a novel automatic platform-based system synthesis procedure, inspired by techniques developed in the context of automatic system verification known as Satisfiability Modulo Theories. It tightly couples the computation of a feasible allocation and binding with nonfunctional constraint checking where, in contrast to existing approaches, not only linear constraints but even nonlinear constraints are supported. This allows to efficiently prove whether there exists a feasible implementation of a set of applications on the given platform with respect to both, functional and nonfunctional constraints. Moreover, an approach for early learning based on feasibility checking of partial implementations is proposed that can significantly improve the synth...

• Type: Journal
• Year: 2010
• Where: CODES
• Authors: Felix Reimann, Michael Glaß, Christian Haubelt, Michael Eberl, Jürgen Teich
• Keywords: CODES 2010, Nonfunctional Constraints, Nonlinear Timing Constraints, Satisfiability Modulo Theories, Software Engineering