Contexte

Le département ISET explore depuis quelques années une piste de recherche qui vise à évaluer la capacité des modèles de systèmes à événements discrets – habituellement utilisés pour l’automatisation et la vérification de propriétés – pour l’ordonnancement d’ateliers hybrides (flowshop/jobshop/openshop) et de manière plus générale pour l’aide à la décision. Ces outils basés sur des automates temporisés permettent notamment de proposer des patrons de modélisation génériques d’ateliers de production présentant des avantages vis-à-vis des approches classiques pour l’ordonnancement (généricité de la modélisation pour différents types de problème d’ordonnancement, modélisation de la dynamique des systèmes notamment)

Objectifs scientifiques

L’objectif de TABS est de fournir un démonstrateur logiciel autour des travaux de recherche présentés précédemment et de le rendre accessible à la communauté scientifique. Il doit faciliter également l’expérimentation des résultats de l’équipe.

Dans le domaine des systèmes à événements discrets (SED), plusieurs modèles ont fait leur preuve pour prendre en compte les perturbations dans l’évaluation et/ou la génération d’ordonnancements. Dans le domaine de la sûreté et de la sécurité, les modèles et outils SED sont généralement utilisés pour évaluer la fiabilité, la disponibilité, la maintenabilité. Ainsi, ils ont prouvé leur efficacité pour la modélisation de systèmes stochastiques et dynamiques et pour la vérification de propriétés sur ces systèmes. Les systèmes à événements discrets présentent ainsi des atouts considérables faisant d’eux de bons candidats pour résoudre le problème d’ordonnancement.

La prise en compte des perturbations a été également traitée en utilisant les modèles et outils SED. En effet, les aléas peuvent être modélisés par l’occurrence d’un événement et les incertitudes par des variables évoluant dans un intervalle. L’objectif de TABS est de fournir un démonstrateur logiciel autour des travaux de recherche présentés précédemment et de le rendre accessible à la communauté scientifique pour cela il doit permettre :

— d’illustrer la capacité des travaux du CRAN à modéliser tout type d’atelier, tout type de perturbation temporelle en permettant de saisir aisément les caractéristiques d’un problème et en générant les modèles automates associés
— d’illustrer la génération d’ordonnancement par model-checking en générant automatiquement la propriété à vérifier et en présentant l’ordonnancement généré sous forme graphique
— d’illustrer l’évaluation de différents critères de robustesse en permettant la sélection du critère, en générant et en vérifiant automatiquement la propriété associée par model-checking stochastique

Description

Le logiciel s’appuie au maximum sur les composants disponibles. Ainsi, l’évaluation des propriétés des automates temporisé est déléguée au logiciel UppAal ⁴³. Tabs 2.0 offre aux utilisateurs une interface permettant de s’abstraire des concepts propres aux systèmes à événements discrets pour ne manipuler que des objets « métiers », du domaine de l’ordonnancement et de la robustesse.

D’un point de vue technologique, le logiciel est basé sur la plateforme logicielle Eclipse : celle-ci fourni un ensemble de composants réutilisables permettant de construire rapidement une application indépendante. De plus, le logiciel s’appuie sur les technologie de modelisation de la plateforme eclipse (EMF – Eclipse Modelling Platform), permettant de définir et d’exploiter un modèle de donnée, et sur le composant Sirius, qui permet de définir des diagrammes (et leurs éditeurs graphiques) associés au objets de ce modèle.

Le logiciel s’articule donc en divers composants :

— le modèle, permettant la structuration des problèmes à résoudre, et compremant en particulier un modèle de l’atelier, des divers scenarios de production et de perturbation ;
— la définition, logique et graphique, de diagrammes, tables et arborescence permettant d’éditer ce modèle (figure 78) ;
— un ensemble de fonctions permettant de représenter ce modèle sous la forme d’un ensemble d’automate temporisés, dans un format exploitable par UppAal, et d’en interpréter les résultats ;
— des éléments graphiques spécifiquement développés (figure 78).

Une forge logicielle permet aux membres de l’équipe de collaborer. Dans une nouvelle version récente (2021), le logiciel a été enrichi de fonctions d’évaluation de la robustesse des ordonnancements, dans la suite des travaux de la thèse de S. Himmiche. Cette amélioration a pu être réalisée grâce à l’attribution de deux hommes.mois d’un ingénieur d’appui, suite à un appel à projet interne au laboratoire.

43. UppAal est un logiciel developpé en collaboration entre les universités d’Uppsala en Suède et celle d’Aalborg au Danemark. Il est gratuit pour les utilisations académiques non-commerciales.