HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 12:42:53 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Links full text


  • HAL Id : tel-01750319, version 1



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⟩



Record views