URL du projet : http://boinc.vgtu.lt/vtuathome/
|
Liens du Projet
|
L'Alliance Francophone
|
Statistiques
|
|
Projet Lituanien, lancé le 13 Avril 2006
VTU@home est une plateforme de calcul distribué mise à la disposition des scientifiques de l'Université Technique Gediminas de Vilnius ainsi que d'autres établissements académiques lituaniens.
La plateforme est gérée par plusieurs scientifiques du département de modélisation mathématique à l'Université Technique Gediminas :
- Le professeur Raimondas Čiegis
- Le docteur Vadimas Starikovičius
- Aurimas Norkevičius (diplomé d'une maitrise de sciences)
Leur rôle est de convertir les scientifiques lituaniens au calcul partagé et de les accompagner dans la préparation de leurs applications pour qu'elles soient compatibles au format du calcul partagé.
Actuellement, vous pouvez participer à un projet axé sur la sécurité des systèmes à forte composante logicielle. D'autres applications sont en cours de développement.
Description de l'application actuelle (VGTU BOINC project client application 6.02)
Notre vie de tous les jours devient de plus en plus tributaire des systèmes à forte composante logicielle: aérospatiale, ferroviaire, automobile, médecine. Les logiciels qui contrôlent les appareils utilisés dans ces domaines sont des bons exemples de l'importance du développement de systèmes de sécurité performants. Il est incontestable que notre capacité à détecter les dysfonctionnements à l'intérieur de ces systèmes (logiciels et appareils) est extrêmement important. Les tests de vacuité, les vérifications de propriétés et les validations sont prioritaires lorsque que l'on envisage le développement de ces systèmes.
Le "Model Checking" (la vérification par modélisation) désigne une famille de techniques de vérification automatique des systèmes dynamiques. Des méthodes formelles adaptées pour préparer toute une batterie de tests a posteriori permettent de s'assurer du bon fonctionnement de toutes sortes de systèmes. On estime que 30 à 70 % des coûts de développement sont liés aux efforts de vérification de ces systèmes. Un modèle mathématique chargé de la vérification des protocoles considère toutes les combinaisons possibles d'un système, c'est à dire tous les états initiaux et tous les états successeurs qui résultent de ces états initiaux. Puis il détermine si un ensemble de propriétés spécifiées est réalisable ou non. La principale difficulté de ces techniques de vérification par modélisation mathématique sont connus sous le nom d'explosion combinatoire. Le besoin en terme de puissance de calcul et la mémoire vive requise par ces vérifications se développent de façon exponentielle en fonction de la taille des systèmes vérifiés. A partir de ce constat, les projets de calcul distribués peuvent mobiliser un grand nombre d'ordinateurs de façon efficiente (et unique!) pour mener à bien ces importants tests de vacuité.
Actuellement, l'application (version 6) résout (calcule) un problème proposé par le professeur R. Šeinauskas, un collègue de l'Institut de développement des technologies de l'information (Université Technologique de Kaunas). Le système admet 206 états initiaux et 107 états successeurs (résultant de ces états initiaux). Pour chaque état initial (au nombre de 206, avec "0" ou "1" pour chaque état initial), le système produit un état successeur (au nombre de 107, avec "0" ou "1" pour chaque état successeur). On considère que les états initiaux, notés "i" et les états successeurs, notés "j", sont corrélés si la modification de "i" entraine une modification de "j". L'objectif est de découvrir toutes les relations (ou tout du moins le maximum de relations) qui peuvent apparaitre dans le système en cours de vérification. Une description plus détaillée du problème est disponible en anglais dans les publications suivantes : [1], [2]
Le problème consiste à trouver toutes les relations dont nous aurons besoin pour vérifier tous les états initiaux. Ces états initiaux sont au nombre de 2206, il est donc biensur impossible de tous les vérifier. Actuellement, le projet utilise la méthode de Monte Carlo (proposée par le Professeur R. Čiegis, Université Technique Gediminas). Chaque unité de calcul teste un nombre donné d'états initiaux, générés de façon aléatoire grâce à la méthode de Monte Carlo pour un nombre minimal de paramètres donnés. Une fois que le calcul est terminé, l'unité de calcul retourne la matrice des relations découvertes (206x107). Cette matrice sera combinée aux matrices obtenues précédemment suite au calcul des autres unités de calcul.
La plateforme est gérée par plusieurs scientifiques du département de modélisation mathématique à l'Université Technique Gediminas :
- Le professeur Raimondas Čiegis
- Le docteur Vadimas Starikovičius
- Aurimas Norkevičius (diplomé d'une maitrise de sciences)
Leur rôle est de convertir les scientifiques lituaniens au calcul partagé et de les accompagner dans la préparation de leurs applications pour qu'elles soient compatibles au format du calcul partagé.
Actuellement, vous pouvez participer à un projet axé sur la sécurité des systèmes à forte composante logicielle. D'autres applications sont en cours de développement.
Description de l'application actuelle (VGTU BOINC project client application 6.02)
Notre vie de tous les jours devient de plus en plus tributaire des systèmes à forte composante logicielle: aérospatiale, ferroviaire, automobile, médecine. Les logiciels qui contrôlent les appareils utilisés dans ces domaines sont des bons exemples de l'importance du développement de systèmes de sécurité performants. Il est incontestable que notre capacité à détecter les dysfonctionnements à l'intérieur de ces systèmes (logiciels et appareils) est extrêmement important. Les tests de vacuité, les vérifications de propriétés et les validations sont prioritaires lorsque que l'on envisage le développement de ces systèmes.
Le "Model Checking" (la vérification par modélisation) désigne une famille de techniques de vérification automatique des systèmes dynamiques. Des méthodes formelles adaptées pour préparer toute une batterie de tests a posteriori permettent de s'assurer du bon fonctionnement de toutes sortes de systèmes. On estime que 30 à 70 % des coûts de développement sont liés aux efforts de vérification de ces systèmes. Un modèle mathématique chargé de la vérification des protocoles considère toutes les combinaisons possibles d'un système, c'est à dire tous les états initiaux et tous les états successeurs qui résultent de ces états initiaux. Puis il détermine si un ensemble de propriétés spécifiées est réalisable ou non. La principale difficulté de ces techniques de vérification par modélisation mathématique sont connus sous le nom d'explosion combinatoire. Le besoin en terme de puissance de calcul et la mémoire vive requise par ces vérifications se développent de façon exponentielle en fonction de la taille des systèmes vérifiés. A partir de ce constat, les projets de calcul distribués peuvent mobiliser un grand nombre d'ordinateurs de façon efficiente (et unique!) pour mener à bien ces importants tests de vacuité.
Actuellement, l'application (version 6) résout (calcule) un problème proposé par le professeur R. Šeinauskas, un collègue de l'Institut de développement des technologies de l'information (Université Technologique de Kaunas). Le système admet 206 états initiaux et 107 états successeurs (résultant de ces états initiaux). Pour chaque état initial (au nombre de 206, avec "0" ou "1" pour chaque état initial), le système produit un état successeur (au nombre de 107, avec "0" ou "1" pour chaque état successeur). On considère que les états initiaux, notés "i" et les états successeurs, notés "j", sont corrélés si la modification de "i" entraine une modification de "j". L'objectif est de découvrir toutes les relations (ou tout du moins le maximum de relations) qui peuvent apparaitre dans le système en cours de vérification. Une description plus détaillée du problème est disponible en anglais dans les publications suivantes : [1], [2]
Le problème consiste à trouver toutes les relations dont nous aurons besoin pour vérifier tous les états initiaux. Ces états initiaux sont au nombre de 2206, il est donc biensur impossible de tous les vérifier. Actuellement, le projet utilise la méthode de Monte Carlo (proposée par le Professeur R. Čiegis, Université Technique Gediminas). Chaque unité de calcul teste un nombre donné d'états initiaux, générés de façon aléatoire grâce à la méthode de Monte Carlo pour un nombre minimal de paramètres donnés. Une fois que le calcul est terminé, l'unité de calcul retourne la matrice des relations découvertes (206x107). Cette matrice sera combinée aux matrices obtenues précédemment suite au calcul des autres unités de calcul.
Bibliographie
1) Bareisa, E.; Jusas, V.; Motiejunas, K.; Seinauskas, R.
The Criteria of Functional Delay Test Quality Assessment.
Proceedings 10th EUROMICRO Conference on Digital System Design, Architectures, Methods and Tools (DSD 2007). 2007, pp. 207-214, ISBN:0-7695-2978-X.
2) Bareisa, E.; Jusas, V.; Motiejunas, K.; Seinauskas, R.
Transition Fault Test Reuse.
Digital System Design: Architectures, Methods and Tools, 2006.
DSD 2006, 9th EUROMICRO Conference. pp. 323-330.
Vidéo de présentation du "model checking" par Jospeh Sifakis, prix Turing 2007