Definition of formal models for heterogeneous timed systems and ther application for job-shop scheduling problem

Actuellement, les méthodes formelles sont de plus en plus utilisées dans le but d’analyser le comportement des systèmes temporisés. Elles visent à améliorer la qualité des systèmes étudiés. Notre travail s’inscrit dans le cadre de la spécification et l’analyse basées sur les méthodes formelles des systèmes temporisés exécutés sur des plateformes réelles. Dans ces plateformes, d’une part, le nombre de machines est d’abord limité, et d’autre part, leurs vitesses peuvent être différentes. Une conséquence de telles plateformes est que la durée d’exécution de chaque action des systèmes étudiés dépend de la machine sur laquelle elle s’exécute, et généralement les exécutions se déroulent de manière conflictuelle sur les machines partagées sans ou avec préemption entre les actions. A cet effet, nous essayons de profiter des avantages offerts par l’une des sémantiques de vrai parallélisme en l’appliquant pour développer des modèles formels dédiés à la spécification et l’analyse des systèmes temporisés hétérogènes. Ces modèles sont appelés raTA (resource allocation Timed Automata) et S-raTA (Stop-watch raTA). Nous proposons d’abord une méthode de génération de ces structures à partir d’une extension du langage Basic LOTOS. Nous montrons par la suite comment les structures proposées peuvent être adaptées pour modéliser et analyser des problèmes d’ordonnancement de type job-shop sans ou avec préemption.Currently, formal methods are increasingly used in order to analyze the behavior of timed systems. They aim to improve the quality of the studied systems. Our work belongs to the area of the specification and analysis based on formal methods of timed systems running on real platforms. In such platforms, the number of machines is limited, and their speeds may be different. As a consequence of such platforms is that the execution time of each action of the studied systems depends on the machine on which it is executed, and executions are generally confrontational on shared machines with or without pre-emption between actions. To this end, we try to take advantage of one of true concurrency semantics by applying it to develop formal models dedicated to the specification and analysis of heterogeneous timed systems. These models are called raTA (resource allocation Timed Automata) and S-raTA (Stop-watch raTA). Firstly, we propose a generation method of these structures from an extension of Basic LOTOS language. We show later how the proposed structures can be adapted to model and analyze scheduling problems of the kind job shop with or without pre-emption