Pruning Infeasible Paths for Tight WCRT Analysis of Synchronous Programs

Abstract : Synchronous programs execute in discrete instants, called ticks. For real-time implementations, it is important to statically determine the worst case tick length, also known as the worst case reaction time (WCRT). While there is a considerable body of work on the timing analysis of procedural programs, such analysis for synchronous programs has received less attention. Current state-of-the art analyses for synchronous programs use integer linear programming (ILP) combined with path pruning techniques to achieve tight results. These approaches first convert a concurrent synchronous program into a sequential program. ILP constraints are then derived from this sequential program to compute the longest tick length. In this paper, we use an alternative approach based on model checking. Unlike conventional programs, synchronous programs are concurrent and state-space oriented, making them ideal for model checking based analysis. We propose an analysis of the abstracted state-space of the program, which is combined with expressive data-flow information, to facilitate effective path pruning. We demonstrate through extensive experimentation that the proposed approach is both scalable and about 67% tighter compared to the existing approaches.
Type de document :
Communication dans un congrès
DATE, Mar 2011, Grenoble, France. 2011
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger
Contributeur : Alain Girault <>
Soumis le : vendredi 24 juin 2011 - 15:22:53
Dernière modification le : jeudi 11 janvier 2018 - 06:22:02
Document(s) archivé(s) le : dimanche 25 septembre 2011 - 02:23:35


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00603287, version 1



Sidharta Andalam, Partha Roop, Alain Girault. Pruning Infeasible Paths for Tight WCRT Analysis of Synchronous Programs. DATE, Mar 2011, Grenoble, France. 2011. 〈inria-00603287〉



Consultations de la notice


Téléchargements de fichiers