Test fonctionnel de propriétés hybrides

On nomme systemes hybrides les systemes qui integrent des comportements continus et discrets. Leur comportement est en partie determine par des contraintes temporelles et/ou leur interaction avec un environnement physique via l'utilisation de capteurs et d'actionneurs. Il peut s'agir par exemple d'equipements de controle de procedes industriels ou de services domotiques. La validation de ces systemes est un probleme crucial, car ils sont parfois utilises au sein d'applications ou la surete de fonctionnement est critique (un systeme critique est un systeme dont la defaillance peut entrainer des blessures ou la mort d'etres humains). Cette validation souleve plusieurs problemes ; en particulier, une description detaillee du systeme a valider n'est pas toujours disponible, ou celle-ci est trop complexe pour qu'il soit possible en pratique d'etablir avec certitude sa correction (par exemple parce que cette verification exhaustive necessite des ressources en temps ou en materiel trop importantes). Dans ces conditions, nous nous interessons a la validation de systemes hybrides specifies par un ensemble de proprietes de surete. Une propriete de surete est une exigence portant sur le comportement du systeme qui ne contraint pas entierement ce comportement, mais en specifie des aspects particuliers. Elle peut ainsi porter sur la reaction attendue du systeme en reponse a une suite d'evenements donnee, ou imposer des limites a l'evolution des grandeurs environnementales qu'il controle. Le travail presente dans ce document consiste en une approche de test fonctionnel, destinee a permettre la validation de systemes hybrides pour lesquels on dispose d'une specification composee de proprietes de surete. La validation consiste a verifier que le systeme satisfait a sa specification, et donc aux besoins qui motivent sa creation (sous reserve que la specification traduise correctement les besoins).