Contribution à l'analyse des TIOSMs pour la vérification de propriétés temporelles de systèmes complexes

Abstract : This thesis deals with validation techniques suited to real time complex applications, that is applications for which we must assure temporal properties in a deterministic way, and which are characterised by their distribution and a co-operative development process. ln this context, we propose methods and tools for their validation both by a priori analysis approach and formaI generation of timed test sequences. The two approach are based on the same formalism named "Timed Input Output State Machine" (TIOSM). The studies led to several results. For a priori validation stage, we specified and implement an enumerative technique for the accessibility graph computation applied to several communicatfng TIOSM and an algorithm for the "on the fly" temporal verification. For the test stage, we implemented a formaI generation of timed test sequences, named adaptive tester and which main property is the decrease of inconclusive verdict number. More, we proposed a hybrid validation method by a co-ordinated use of exhaustive analysis on critical parts of a system and simulation applied to the complete system. Finally we developed model translations (TIOSM form and to Temporal Petri Nets, TIOSM to SDL).
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/INPL_T_2001_KAISER_L.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01750319
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:42:53 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:18 PM

Identifiers

  • HAL Id : tel-01750319, version 1

Collections

Citation

Laurent Kaiser. Contribution à l'analyse des TIOSMs pour la vérification de propriétés temporelles de systèmes complexes. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2001. Français. ⟨NNT : 2001INPL010N⟩. ⟨tel-01750319⟩

Share

Metrics

Record views

13