Efficient Parametric Verification of Parametric Timed Automata
Institution:
Sorbonne Paris CitéDisciplines:
Directors:
Abstract EN:
Critical real-time systems are becoming ubiquitous and are playing a vital role in our world. To provide guarantees that the system is behaving correctly, the correctness of these systems need to be verified before running. Besides functional checking, the timed behavior checking is also crucial. Indeed, the correctness of the systems also depends on the timing values or delays of internal operations that can be affected by the environment. Verification techniques assure that software or hardware systems fully satisfy all their expected requirements. Most formal verification methods for timed systems guarantee the correctness of a timed system for the predefined timing values in its blueprint, but not for other undefined timing values which might occur by the environment change and lead to undesired system behaviors. Unfortunately, verifying such system for various timing values can be an obstacle and time-consuming. Therefore, by abstracting these specific timing values with parameters, many timing values of a system can be easily synthesized and checked at the same time : this technique is also known as parameter synthesis. As a huge challenge for the verification, parameter synthesis techniques also suffer from the “state space explosion” problem, which is the explosion of the number of possible states while verifying a system formally. Firstofall, we are interested in taking advantage of the capabilities of current distributed architectures, and parameter synthesis algorithms should be redefined and adapted to the distributed case. We propose in the thesis several distribution schemes that can accelerate our parameter synthesis procedures. We also focus on studying the techniques such as symbolic verification, zone subsumption, etc. and how they affect the state space explosion problem. Then we introduce several smart state exploration techniques with some heuristics, in order to reduce the state space explosion. These techniques and heuristics are integrated into our new synthesis algorithms, and one of these algorithms is also extended in a distributed manner which gives an impressive performance in our benchmarks. Furthermore, to achieve a reliable result we present an approach for detecting timed systems doing an infinite amount of actions in a finite time, which is known as the Zeno phenomenon in theory. In reality, it is infeasible and such counterexamples should always be avoided. Additionally, to detect the non-Zeno phenomenon on a large scale network model, we also distribute our approach on clusters. In the end, we introduce an algorithm to detect non-Zeno runs and its distributed version of it for large-scale models. At the time of writing this thesis, this is also the first work on non-Zeno parameter synthesis.
Abstract FR:
Les systèmes temps-réel critiques deviennent de plus en plus ubiquitaires et jouent un rôle majeur de nos jours. Pour garantir le bon comportement d’un système, leur correction doit être vérifiée avant les mises en service opérationnel. Outre la vérification fonctionnelle, la vérification du comportement temporel est également cruciale. Les tech niques de vérification garantissent que les systèmes logiciels ou matériels satisfont les contraintes attendues. La plupart des méthodes de vérification formelle pour les systèmes temporisés garantissent leur correction pour des valeurs prédéfinies des contraintes temporelles, mais pas pour d’autres valeurs non définies a priori, dues par exemple à un changement de l’environnement, et qui peuvent conduire à des comportements du système non désirés. Malheureusement, la vérification de tels systèmes pour différentes valeurs temporelles peut être un obstacle et coûteuse en temps. Ainsi, en s’abstrayant de valeurs temporelles spécifiques à l’aide de paramètres, de nombreuses valeurs temporelles d’un système peuvent être synthétisées et vérifiées simultanément : cette technique est la synthèse de paramètres. Les techniques de synthèse de paramètres constituent un défi majeur pour la vérification. Elles souffrent du problème de l’explosion combinatoire de l’espace d’´états, c’est-a`-dire de la génération d’un nombre d’´états considérable lors de la vérification formelle du système. Dans un premier temps, nous nous sommes intéressés à tirer parti des spécificités des architectures informatiques distribuées modernes. Ainsi, les algorithmes de synthèse de paramètres ont dû être redéfinis et adaptés au cas distribué. Nous proposons dans cette thèse différents schémas de distribution pour accélérer les procédures de synthèse de paramètres. Nous nous intéressons également à l’étude de techniques telles que la vérification symbolique, la subsomption, etc. et à leur impact sur l’explosion de l’espace d’états. Nous introduisons donc ensuite plusieurs heuristiques d’exploration afin de réduire l’explosion de l’espace d’états. Celles-ci sont intégrées a` nos nouveaux algorithmes de synthèse de paramètres. L’un de ces algorithmes est étendu de manière distribuée, conduisant `a des performances spectaculaires dans nos expérimentations. Enfin, pour obtenir un résultat réalisable, nous présentons une approche qui détecte des systèmes temporisés effectuant un nombre infini d’actions en un temps fini, connu sous le nom de phénomène Zeno. En pratique, de tels comportements ne peuvent pas avoir lieu, et ne constituent pas des contre-exemples effectifs. De plus, nous proposons une approche distribuée pour détecter des phénomènes non Zeno à large échelle. Nous introduisons un algorithme détectant des comportements non Zeno, ainsi que sa version distribuée. Au moment de l’écriture de cette thèse, ceci constitue les premiers résultats sur la synthèse de paramètres non Zeno.