Optimized implementation of synchronous models on industrial LTTA systems

Marco Di Natale*, Qi Zhu, Alberto Sangiovanni-Vincentelli, Stavros Tripakis

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

4 Scopus citations


Synchronous models are used to specify embedded systems functions in a clear and unambiguous way and allow verification of properties using formal methods. The implementation of a synchronous specification on a distributed architecture must preserve the model semantics to retain the verification results. Globally synchronized time-triggered architectures offer the simplest implementation path, but can be inefficient or simply unavailable. In past work, we defined a mapping of synchronous models on a general class of distributed asynchronous architectures, for which the only requirement is a lower bound on the rate of activation of tasks. In this paper, we set tighter requirements on task execution rates, and we include a realistic modeling of communication delays, task scheduling delays and schedulability conditions, discussing the timing characteristics of an implementation on a system with a Controller Area Network (CAN). Next, the semantics preservation conditions are formulated as constraints in an architecture optimization problem that defines a feasible task model with respect to timing constraints. An automotive case study shows the applicability of the approach and provides insight on the software design elements that are critical for a feasible implementation.

Original languageEnglish (US)
Pages (from-to)315-328
Number of pages14
JournalJournal of Systems Architecture
Issue number4
StatePublished - Apr 2014


  • Code generation
  • Distributed systems
  • Embedded systems
  • Loosely time-triggered architecture
  • Semantics-preserving implementation
  • Synchronous models

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture


Dive into the research topics of 'Optimized implementation of synchronous models on industrial LTTA systems'. Together they form a unique fingerprint.

Cite this