Validation d''un modèle basé sur les rdpt

Les syst mes temps r el impliquent la prise en charge des contraintes temporelles diverses. Elles peuvent tre fortes ou faibles; exprimant des relations de synchronisation, de priorit voire de pr emption temporelle. Par ailleurs, ces syst mes peuvent n cessiter des ressources aussi bien critiques que non critiques. Nous explorons dans cette th se un mod le g n ral bas sur les r seaux de Petri temporels, permettant une prise en charge exhaustive de ces diff rentes contraintes. Ce mod le appel STPTPN (synchronizing Transitions Preemptive Time Petri Net), offre un cadre formel dans lequel les syst mes les plus complexes peuvent tre sp cifi s. Plus encore, nous d veloppons une approche d'analyse par num ration de l'espace d' tat d'un tel mod le. Nous montrons comment interpr ter les propri t's g n rales du mod le partir des graphes obtenus et proposons une technique efficace pour l'estimation de la r ponse du temps born . De plus, les applications multim dia tant dans, nous motivons un certain nombre de nos propositions par leur exploitation dans la v rification de la consistance des documents multim dia.