Model-checking symbolique pour la verification de systemes et son application aux tables de decision et aux systemes d'editions collaboratives distribuees

This thesis is related to a research which aims at applying one specific formal method in program and requirements analysis: symbolic execution intertwined with model checking. This technique has known a major development in the past few years, thus raising interest among researchers in the field.;In the present work, we apply this technique using the extension Symbolic JPF of the software model checker Java PathFinder. Our choice relies on the high level of maturity of the tool in the verification of a wide range of applications. Thus, using this tool, we direct our verification purposes on two different applications albeit both end up in one unique outcome: counterexamples representing input test cases refuting some property. It is to be noted that the verification process handles several classes of properties ranging from application-dependent to application-independent properties.;In fact, our first goal is to verify reachability and invariance properties in the context of a flight simulator especially modelled in a well-known formal tabular notation---decision tables. These tables concisely point out the relations between system input variables or conditions and system output variables corresponding to the resulting actions.;However, those encountered decision tables had to respect some hierarchy: One table's output variables could be fed as input variables to other tables. Accordingly, we were compelled to follow a specific computation order imposed by the tables' structure.;Therefore, symbolic execution along with model checking is a resulting approach enforced with advantages of both techniques. This yields a higher degree of interpreting the retrieved flaws provided through generated counterexamples, for even the most sophisticated systems.;Moreover, one of the challenges encountered during the verification of such systems resides in its computation process which includes random and complex arithmetic and trigonometric operations. More specifically, in the context of such systems with infinite domains, model checking is constrained with the state explosion problem due to the exhaustive state exploration in the verification of property violations. Taking into account the latter limitation, our combined approach of symbolic execution with model checking allows the abstraction of computed variables, thus drastically reducing the number of explored states. As a result, the identification of critical cases violating special system properties is made possible. Those generated cases identify the specific combinations of system input variables disproving the verified property. The applied approach in our case study framework is original in the verification of decision tables modelling a system governed by non-linear constraints.;In such systems, users on each site could modify the shared object by some exchange of editing operations in concurrent and consecutive fashions. As a consequence, a divergence in the contents of the replicas between different users is possible leading to the system inconsistence. This contradicts with the main purpose of such systems that originally allows a collaborative interaction between users while preserving the copies convergence in each site. This convergence is allegedly ensured by the application of operational transformations, under special conditions, through well-defined integration algorithms.;In our case study framework, the applied approach of symbolic execution combined with model-checking resulted in generating input test cases illustrating the divergence scenarios for all five considered algorithms. Since formally verifying such systems is still limited, we could say that our approach is original in collecting all retrieved counterexamples violating the convergence property. Moreover, another major contribution in our work was in the use of further abstractions in the description of the previous system model. Hence, using this abstract model, we gained in both execution time and memory space relatively to the previous approach. (Abstract shortened by UMI.)...