Techn. University, Diss., 2001--Berlin.

Techn. Hochsch., Diss., 2001--Aachen.

Techn. University, Diss., 2003--Berlin.

University, Diss., 2002--Saarbrücken.

Ces dernières années, l'analyse de systèmes complexes critiques est devenue de plus en plus importante. En particulier, l'analyse quantitative de tels systèmes est nécessaire afin de pouvoir garantir que leur probabilité d'échec est très faible. La difficulté de l'analyse de ces systèmes réside dans le fait que leur espace d’état est très grand et que la probabilité recherchée est extrêmement petite, de l'ordre d'une chance sur un milliard, ce qui rend les méthodes usuelles inopérantes. Les algorithmes de Model Checking quantitatif sont les algorithmes classiques pour l'analyse de systèmes probabilistes. Ils prennent en entrée le système et son comportement attendu et calculent la probabilité avec laquelle les trajectoires du système correspondent à ce comportement. Ces algorithmes de Model Checking ont été largement étudié depuis leurs créations. Deux familles d'algorithme existent : - le Model Checking numérique qui réduit le problème à la résolution d'un système d'équations. Il permet de calculer précisément des petites probabilités mais soufre du problème d'explosion combinatoire- - le Model Checking statistique basé sur la méthode de Monte-Carlo qui se prête bien à l'analyse de très gros systèmes mais qui ne permet pas de calculer de petite probabilités. La contribution principale de cette thèse est le développement d'une méthode combinant les avantages des deux approches et qui renvoie un résultat sous forme d'intervalles de confiance. Cette méthode s'applique à la fois aux systèmes discrets et continus pour des propriétés bornées ou non bornées temporellement. Cette méthode est basée sur une abstraction du modèle qui est analysée à l'aide de méthodes numériques, puis le résultat de cette analyse est utilisé pour guider une simulation du modèle initial. Ce modèle abstrait doit à la fois être suffisamment petit pour être analysé par des méthodes numériques et suffisamment précis pour guider efficacement la simulation. Dans le cas général, cette abstraction doit être construite par le modélisateur. Cependant, une classe de systèmes probabilistes a été identifiée dans laquelle le modèle abstrait peut être calculé automatiquement. Cette approche a été implémentée dans l'outil Cosmos et des expériences sur des modèles de référence ainsi que sur une étude de cas ont été effectuées, qui montrent l'efficacité de la méthode. Cette approche à été implanté dans l'outils Cosmos et des expériences sur des modèles de référence ainsi que sur une étude de cas on été effectué, qui montre l'efficacité de la méthode. / In the past decades, the analysis of complex critical systems subject to uncertainty has become more and more important. In particular the quantitative analysis of these systems is necessary to guarantee that their probability of failure is very small. As their state space is extremly large and the probability of interest is very small, typically less than one in a billion, classical methods do not apply for such systems. Model Checking algorithms are used for the analysis of probabilistic systems, they take as input the system and its expected behaviour, and compute the probability with which the system behaves as expected. These algorithms have been broadly studied. They can be divided into two main families: Numerical Model Checking and Statistical Model Checking. The former computes small probabilities accurately by solving linear equation systems, but does not scale to very large systems due to the space size explosion problem. The latter is based on Monte Carlo Simulation and scales well to big systems, but cannot deal with small probabilities. The main contribution of this thesis is the design and implementation of a method combining the two approaches and returning a confidence interval of the probability of interest. This method applies to systems with both continuous and discrete time settings for time-bounded and time-unbounded properties. All the variants of this method rely on an abstraction of the model, this abstraction is analysed by a numerical model checker and the result is used to steer Monte Carlo simulations on the initial model. This abstraction should be small enough to be analysed by numerical methods and precise enough to improve the simulation. This abstraction can be build by the modeller, or alternatively a class of systems can be identified in which an abstraction can be automatically computed. This approach has been implemented in the tool Cosmos, and this method was successfully applied on classical benchmarks and a case study.

Les automates d'arbres et leurs applications à la vérification forment le tronc commun de cette thèse. Dans la première parie, nous définissons une plate forme de model-checking complète [...] La seconde partie se penche sur un aspect important des automates que nous utilisons: leur contraintes [...] Finalement, nous étudions également les automates d'arbres cheminants [...] Nous améliorons leur conversion en automates parallèles, et nous développons une procédure de semi décision de leur vacuité, à la fois efficace et précise / Tree automata, and their applications to verification from the common thread of this thesis In the first part, we definie a complete model-cheking framework.[...] The second part focus on an important aspect of the automata involved: constraints.[...] Finaly, we also study the very different variety of tree-walking automata which have tight connections with navigational languages on semi-structured documents.

The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.

Reliable operation of every day use computing system, from simple coffee machines to complex flight controller system in an aircraft, is necessary to save time, money, and in some cases lives. System testing can check for the presence of unwanted execution but cannot guarantee the absence of such. Probabilistic model checking techniques have demonstrated significant potential in verifying performance and reliability of various systems whose execution are defined with likelihood. However, its inability to scale limits its applicability in practice. This thesis presents a new model checker, STAMINA, with efficient and scalable model truncation for probabilistic verification. STAMINA uses a novel model reduction technique generating a finite state representations of large systems that are amenable to existing probabilistic model checking techniques. The proposed method is evaluated on several benchmark examples. Comparisons with another state-of-art tool demonstrates both accuracy and efficiency of the presented method.

No description available.

A stochastic shortest path problem is an undiscounted infinite-horizon Markov decision process with an absorbing and costree target state, where the objective is to reach the target state while optimizing total expected cost. In almost all cases, the objective in solving a stochastic shortest path problem is to minimize the total expected cost to reach the target state. But in probabilistic model checking, it is also useful to solve a problem where the objective is to maximize the expected cost to reach the target state. This thesis considers the maximum-time stochastic shortest path problem, which is a special case of the maximum-cost stochastic shortest path problem where actions have unit cost. The contribution is an efficient approach to computing high-quality bounds on the optimal solution for this problem. The bounds are useful in themselves, but can also be used by other algorithms to accelerate search for an optimal solution.