test
Search publications, data, projects and authors

Thesis

English

ID: <

10670/1.weo1at

>

Where these data come from
Verification of Weakly-Hard Requirements on Quasi-Synchronous Systems

Abstract

The synchronous approach to reactive systems, where time evolves by globally synchronized discrete steps, has proven successful for the design of safetycriticalembedded systems. Synchronous systems are often distributed overasynchronous architectures for reasons of performance or physical constraintsof the application. Such distributions typically require communication and synchronizationprotocols to preserve the synchronous semantics. In practice, protocolsoften have a significant overhead that may conflict with design constraintssuch as maximum available buffer space, minimum reaction time, and robustness.The quasi-synchronous approach considers independently clocked, synchronouscomponents that interact via communication-by-sampling or FIFO channels. Insuch systems we can move from total synchrony, where all clocks tick simultaneously,to global asynchrony by relaxing constraints on the clocks and withoutadditional protocols. Relaxing the constraints adds different behaviors dependingon the interleavings of clock ticks. In the case of data-flow systems, onebehavior is different from another when the values and timing of items in a flowof one behavior differ from the values and timing of items in the same flow ofthe other behavior. In many systems, such as distributed control systems, theoccasional difference is acceptable as long as the frequency of such differencesis bounded. We suppose hard bounds on the frequency of deviating items in aflow with, what we call, weakly-hard requirements, e.g., the maximum numberdeviations out of a given number of consecutive items.We define relative drift bounds on pairs of recurring events such as clockticks, the occurrence of a difference or the arrival of a message. Drift boundsexpress constraints on the stability of clocks, e.g., at least two ticks of one perthree consecutive ticks of the other. Drift bounds also describe weakly-hardrequirements. This thesis presents analyses to verify weakly-hard requirementsand infer weakly-hard properties of basic synchronous data-flow programs withasynchronous communication-by-sampling when executed with clocks describedby drift bounds. Moreover, we use drift bounds as an abstraction in a performanceanalysis of stream processing systems based on FIFO-channels.

Your Feedback

Please give us your feedback and help us make GoTriple better.
Fill in our satisfaction questionnaire and tell us what you like about GoTriple!