A symbolic system synthesis approach for hard real-time systems based on coordinated SMT-solving

Abstract : We propose an SMT-based system synthesis approach where the logic solver performs static binding and routing while the background theory solver computes global time-triggered schedules. In contrast to previous work, we assign additional time to the logic solver in order to refine the binding and routing such that the background theory solver is more likely to find a feasible schedule within a reasonable amount of time. We show by experiments that this coordination of the two solvers results in a considerable reduction of the overall synthesis time.
Type de document :
Communication dans un congrès
W. Nebel; D. Atienza. Proceedings of the Conference on Design, Automation and Test in Europe (DATE'15), 2015, San Jose, United States. ACM, pp.357-362, 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01187000
Contributeur : René Quiniou <>
Soumis le : mardi 25 août 2015 - 18:25:42
Dernière modification le : mardi 16 janvier 2018 - 15:54:11

Identifiants

  • HAL Id : hal-01187000, version 1

Citation

Alexander Biewer, Benjamin Andres, Jens Gladigau, Torsten Schaub, Christian Haubelt. A symbolic system synthesis approach for hard real-time systems based on coordinated SMT-solving. W. Nebel; D. Atienza. Proceedings of the Conference on Design, Automation and Test in Europe (DATE'15), 2015, San Jose, United States. ACM, pp.357-362, 2015. 〈hal-01187000〉

Partager

Métriques

Consultations de la notice

232