Verification of Weakly-Hard Requirements on Quasi-Synchronous Systems
Vérification de propriétés faiblement dures des systèmes quasi-synchrones
Résumé
The synchronous approach to reactive systems, where time evolves by globally synchronized discrete steps, has proven successful for the design of safety-critical embedded systems. Synchronous systems are often distributed over asynchronous architectures for reasons of performance or physical constraints of the application. Such distributions typically require communication and synchronization protocols to preserve the synchronous semantics. In practice, protocols often have a significant overhead that may conflict with design constraints such as maximum available buffer space, minimum reaction time, and robustness. The quasi-synchronous approach considers independently clocked, synchronous components that interact via communication-by-sampling or FIFO channels. In such systems we can move from total synchrony, where all clocks tick simultaneously, to global asynchrony by relaxing constraints on the clocks and without additional protocols. Relaxing the constraints adds different behaviors depending on the interleavings of clock ticks. In the case of data-flow systems, one behavior is different from another when the values and timing of items in a flow of one behavior differ from the values and timing of items in the same flow of the other behavior. In many systems, such as distributed control systems, the occasional difference is acceptable as long as the frequency of such differences is bounded. We suppose hard bounds on the frequency of deviating items in a flow with, what we call, weakly-hard requirements, e.g., the maximum number deviations out of a given number of consecutive items. We define relative drift bounds on pairs of recurring events such as clock ticks, the occurrence of a difference or the arrival of a message. Drift bounds express constraints on the stability of clocks, e.g., at least two ticks of one per three consecutive ticks of the other. Drift bounds also describe weakly-hard requirements. This thesis presents analyses to verify weakly-hard requirements and infer weakly-hard properties of basic synchronous data-flow programs with asynchronous communication-by-sampling when executed with clocks described by drift bounds. Moreover, we use drift bounds as an abstraction in a performance analysis of stream processing systems based on FIFO-channels.
L'approche synchrone aux systèmes réactifs, où le temps global est une séquence d'instants discrets, a été proposée afin de faciliter la conception des systèmes embarqués critiques. Des systèmes synchrones sont souvent réalisés sur des architectures asynchrones pour des raisons de performance ou de contraintes physiques de l'application. Une répartition d'un système synchrone sur une architecture asynchrone nécessite des protocoles de communication et de synchronisation pour préserver la sémantique synchrone. En pratique, les protocoles peut avoir un coût important qui peut entrer en conflit avec les contraintes de l'application comme, par exemple, la taille de mémoire disponible, le temps de réaction, ou le débit global. L'approche quasi-synchrone utilise des composants synchrones avec des horloges indépendantes. Les composants communiquent par échantillonnage de mémoire partagée ou par des tampons FIFO. On peut exécuter un tel système de façon synchrone, où toutes les horloges avancent simultanément, ou de façon asynchrone avec moins de contraintes sur les horloges, sans ajouter des protocoles. Plus les contraintes sont relâchées, plus de comportements se rajoutent en fonction de l'entrelacement des tics des horloges. Dans le cas de systèmes flots de données, un comportement est différent d'un autre si les valeurs ou le cadencement ont changé. Pour certaines classes de systèmes l'occurrence des déviations est acceptable, tant que la fréquence de ces événements reste bornée. Nous considérons des limites dures sur la fréquence des deviations avec ce que nous appelons les exigences faiblement dures, par exemple, le nombre maximal d'éléments divergents d'un flot par un nombre d'éléments consécutifs. Nous introduisons des limites de dérive sur les apparitions relatives des paires d'événements récurrents comme les tics d'une horloge, l'occurrence d'une difference, ou l'arrivée d'un message. Les limites de dérive expriment des contraintes entre les horloges, par exemple, une borne supérieure de deux tics d'une horloge entre trois tics consécutifs d'une autre horloge. Les limites permettent également de caractériser les exigences faiblement dures. Cette thèse présente des analyses pour la vérification et l'inférence des exigences faiblement dures pour des programmes de flots de données synchrones étendu avec de la communication asynchrone par l'échantillonnage de mémoire partagée où les horloges sont décrites par des limites de dérive. Nous proposons aussi une analyse de performance des systèmes répartis avec de la communication par tampons FIFO, en utilisant les limites de dérive comme abstraction.
Loading...