De nombreux sytèmes critiques comportent des aspects temporisés, où interviennent de manière cruciale des contraintes quantitatives sur les délais séparant certaines actions. Un automate programmable industriel (API) constitue un composant fondamental d'un système souvent critique destiné à réagir et à communiquer en temps réel avec son environnement. Ma thèse se situe dans le contexte de la vérification de propriétés temporisées des APIS. Plus précisement, on propose une sémantique formelle à base d'automates temporisés pour la modélisation d'une sous classe de programmes Ladder comportant des blocs TON. On fournie une logique temporisée dont la sémantique permet de considérer seulement les événements "signifcatifs" (c'est à dire les événements qui durent suffisamment longtemps). On propose deux sémantiques différentes pour cette logique: sémantique "locale" et sémantique "globale". Pour la sémantique "locale", on a obtenu plusieurs résultats d'expressivité et grâce à une nouvelle relation d'équivalence, on montre que son model checking reste décidable sans modifier la complexité théorique. En revanche, pour la sémantique "globale", le model checking devient indécidable.

Cette thèse présente une analyse de la consommation d'énergie des systèmes de contrôlecommande électriques des machines automatisées en vue de réduire leur consommation d'énergie. Il est notamment présenté les notions associées aux systèmes de contrôle-commande et il est développé des méthodes et un simulateur de consommation d'énergie destiné à l'analyse de la consommation d'énergie. A partir de ceci, il est réalisé une analyse selon 3 axes : consommation des composants de contrôlecommande pris individuellement, consommation des systèmes de contrôle-commande selon le type de machine et l'assemblage des composants et enfin, consommation dans le temps selon les modes de marche. Ces travaux mettent en évidence que la consommation des systèmes de contrôle-commande est souvent faible comparée à celle des actionneurs, mais qu'il est tout de même possible de réduire d'un facteur 2 la consommation d'énergie.