Skip to Main content Skip to Navigation
Theses

Preuves par récurrence avec ensembles couvrants contextuels. Applications à la vérification de logiciels de télécommunications

Abstract : The software certification process is in most of the cases a laborious and costly task that needs not only mathematical methods to express clearly and in a structured manner the software's expected behavior but also automatic tools to prove sorne of its properties. Among the proof techniques, induction is well-suited to reason on infinite data structures, like integers and lists, or parameterized systems. This thesis contains a theoretical and an applicative part. The first one is centered around the new concept of contextual cover set (CCS). The principle of induction with cess is reftected by an abstract inference system introducing sufficient conditions for its sound usage. The modular design of concrete inference rules is an advantage of this approach. As a case study, we specify the SPIKE prover as an instance of this system. In the second part, we first analyze the feature interaction problem in telecommunications. We propose a methodology for their detection and resolution by using techniques based on conditional rewriting and induction. In another application, we obtain the first formaI proof of a generic incremental ABR conformance algorithm, by using the PYS prover. Then, we use SPIKE to verify completely automatically the most of the 80 user-defined lemmas.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2000_0111_STRATULAT.pdf
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01746470
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:38:28 AM
Last modification on : Thursday, January 7, 2021 - 11:48:44 AM

Identifiers

  • HAL Id : tel-01746470, version 1

Collections

Citation

Sorin Stratulat. Preuves par récurrence avec ensembles couvrants contextuels. Applications à la vérification de logiciels de télécommunications. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2000. Français. ⟨NNT : 2000NAN10111⟩. ⟨tel-01746470⟩

Share

Metrics

Record views

21