Yang Yang and Stavros Tripakis and Alberto L. Sangiovanni-Vincentelli

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2011-115

October 21, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-115.pdf

Most of the design challenges for complex cyber-physical systems, where a digital controller governs a multi-physics plant, relate to the distributed nature of the systems to be controlled. Cars, airplanes, and power distribution grids are well-known examples. The characteristics of the communication network that connects the system components affect the derivation of the control law and the verification of design correctness. For this reason, there has been a strong interest in using languages and methodologies that facilitate the use of formal methods. These languages and methodologies are mostly based on a synchronous paradigm that, while satisfies the need for formalization, often results in an inefficient implementation requiring substantial overhead when compared to approaches that do not enforce synchronicity on the execution platform. Therefore, the interest is high for techniques that on one hand, maintain the formal properties of synchronous models, and on the other hand, enable the use of asynchronous and distributed execution platforms with little overhead.

In this paper we address the problem of automatic synthesis, and in particular automatic and semantics-preserving implementation of Triggered Synchronous Block Diagrams (SBDs) on distributed, asynchronous execution platforms. This problem was studied for "pure" SBDs (where all blocks are triggered in every synchronous step). The method can be adapted to Triggered SBDs by using trigger elimination, where triggers are transformed to standard inputs. However, this often results in unnecessary communication overhead. In this paper we propose methods to minimize this overhead, thus improving the efficiency of the approach. We consider both general Triggered SBDs where the values of triggers are dynamically computed and are thus not known a-priori, as well as Timed SBDs where triggers are statically known, usually specified by (period, initial phase) pairs.


BibTeX citation:

@techreport{Yang:EECS-2011-115,
    Author= {Yang, Yang and Tripakis, Stavros and Sangiovanni-Vincentelli, Alberto L.},
    Title= {Efficient Distribution of Triggered Synchronous Block Diagrams},
    Year= {2011},
    Month= {Oct},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-115.html},
    Number= {UCB/EECS-2011-115},
    Abstract= {Most of the design challenges for complex cyber-physical systems, where a digital controller governs a multi-physics plant, relate to the distributed nature of the systems to be controlled. Cars, airplanes, and power distribution grids are well-known examples. The characteristics of the communication network that connects the system components affect the derivation of the control law and the verification of design correctness. For this reason, there has been a strong interest in using languages and methodologies that facilitate the use of formal methods. These languages and methodologies are mostly based on a synchronous paradigm that, while satisfies the need for formalization, often results in an inefficient implementation requiring substantial overhead when compared to approaches that do not enforce synchronicity on the execution platform. Therefore, the interest is high for techniques that on one hand, maintain the formal properties of synchronous models, and on the other hand, enable the use of asynchronous and distributed execution platforms with little overhead.

In this paper we address the problem of automatic synthesis, and in particular automatic and semantics-preserving implementation of Triggered Synchronous Block Diagrams (SBDs) on distributed, asynchronous execution platforms. This problem was studied for "pure" SBDs (where all blocks are triggered in every synchronous step). The method can be adapted to Triggered SBDs by using trigger elimination, where triggers are transformed to standard inputs. However, this often results in unnecessary communication overhead. In this paper we propose methods to minimize this overhead, thus improving the efficiency of the approach. We consider both general Triggered SBDs where the values of triggers are dynamically computed and are thus not known a-priori, as well as Timed SBDs where triggers are statically known, usually specified by (period, initial phase) pairs.},
}

EndNote citation:

%0 Report
%A Yang, Yang 
%A Tripakis, Stavros 
%A Sangiovanni-Vincentelli, Alberto L. 
%T Efficient Distribution of Triggered Synchronous Block Diagrams
%I EECS Department, University of California, Berkeley
%D 2011
%8 October 21
%@ UCB/EECS-2011-115
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-115.html
%F Yang:EECS-2011-115