Calcul des états atteignables de programmes ESTEREL partitionné selon la syntaxe
Institution:
NiceDisciplines:
Directors:
Abstract EN:
We consider the issue of exploiting the structural form of Esterel programs to partition the algorithmic RSS (reachable state space) fix-point construction used in model-checking techniques. The basic idea sounds utterly simple, as seen on the case of sequential composition: in P;Q, first compute entirely the states reached in P, and then only carry on to Q, each time using only the relevant transition relation part. Here a brute-force symbolic breadth-first search would have mixed the exploration of P and Q instead, in case P had different behaviors of various lengths, and that would result in irregular BBD representation of temporary state spaces, a major cause of complexity in symbolic model-checking. Difficulties appear in our decomposition approach when scheduling the different transition parts in presence of parallelism and local signal exchanges. Program blocks (or "Macro-states") put in parallel can be synchronized in various ways, due to dynamic behaviors, and considering all possibilities may lead to an excessive division complexity. The goal is here to find a satisfactory trade-off between compositional and global approaches. Concretely we use some of the features of the BDD library, and heuristic orderings between internal signals, to have the transition relation progress through the program behaviors to get the same effect as a global RSS computation, but with much more localized transition applications. We provide concrete benchmarks showing the usefulness of the approach.
Abstract FR:
Le calcul symbolique des états atteignables d'un programme constitue un élément de base dans la compilation des programmes réactifs synchrones. Nous proposons d'améliorer la complexité parfois prohibitive de ce calcul en exploitant la structure des programmes. L'idée de base paraît extrêmement simple: pour le cas P;Q où deux blocs de programme sont combinés en séquence, nous cherchons à construire entièrement les états atteignables de P et de ne s'occuper de Q que lorsque P est complètement exploré. Si les comportements de P étaient de durée variable, le calcul symbolique Breadth First Search aurait combiné l'exploration de P et de Q dans un même mouvement. De ceci aurait résulté une irrégularité dans les représentations intermédiaires des états atteints. Les difficultés de notre approche apparaissent en présence de parallélisme et d'échange de signaux locaux où les blocs de programme peuvent se synchroniser de multiples façons en raison du comportement dynamique du programme. Considérer toutes ces possibilités mènerait à une forte complexité. Le but ici est de trouver un compromis satisfaisant entre l'approche globale Breadth First Search et l'approche compositionnelle partitionnée. Concrètement, nous nous appuyons sur des caractéristiques intéressantes de notre librairie de BDD pour développer une approche efficace. Nous employons des heuristiques permettant de partitionner notre programme et d'ordonnancer la construction des états atteignables afin de calculer exactement les mêmes résultats que par la méthode de base mais en appliquant des fonctions de transition plus localisées. Les premiers résultats expérimentaux montrent la pertinence de notre approche.