Jacques JULLIAND LIFC (Laboratoire d'Informatique de l'Université de Franche-Comté) FRE CNRS 2661 16, routede Gray 25030 BESANCON CEDEX FRANCE Voice : +33 03.81.66.64.51 Fax : +33 03.81.66.64.50 E-mail : julliand@lifc.univ-fcomte.fr

Thème de recherche : Spécification et vérification de logiciels critiques

• Vérification de propriétés PLTL (Logique temporelle linéaire)
• Combinaison preuve et model-checking
• Génération de tests de politique de sécurité
• Méthode B et raffinement
• Automates temporisés et raffinement

• Curriculum Vitae
• Recherche
• Enseignement
• Publications
  

Click here to get the English version 

Jacques JULLIAND Curriculum Vitae

Professeur à l'Université de Franche-Comté, HDR soutenue en février 1992 à l'Université de Nancy 1 : "Une approche applicative de la programmation parallèle asynchrone"

• 1996 - 2007 : Directeur du LIFC
• membre des comités de programme ZB et AFADL
• chair man de AFADL 2004, B'2007
• 1994 -1998 : Responable du DESS Génie Informatique, Systèmes Distribués, Parallélisme
• 1988 - 1992 : Responsable de la licence et de la maîtrsie d'informatique
• 1985 - 1993 : Maître de conférences à l'UFC
• 1992 : HDR à l'Université de Nancy 1
• 1982 - 1985 : Assistant à l'IUT de Belfort
• 1981 : Thèse de 3ème cycle
• 1978 : DEA Université de Nancy 1
• 1972-1977 : Etude d'ingénieur INSA Lyon

Jacques JULLIAND Recherche

Au sein de l'équipe Techniques Formelles et à Contraintes, j'anime des activités de recherche au sein de l'action Expression et Vérification par raffinement.

Notre objectif est de contribuer à améliorer les techniques de vérification de propriétés dynamiques au sein d'un processus de développement par raffinement. Notre démarche est supportée par le langage et la méthode B qui apporte le raffinement et la sémantique axiomatique des substitutions généralisées. On y associe également une sémantique par des systèmes de transition étiquetés afin de combiner preuve et model-checking. Les principales contributions sont les suivantes :

• Raffinement de propriétés de Logique Temporelle Linéaire (LTL). La contribution est une méthode de vérification de propriétés raffinées combinant model-checking (model-checking de la propriété abstraite) et preuve de la propriété raffinée. L'apport est d'effectuer la vérification sans avoir à produire de variant. Voir publications [FASE 2000], [ZB 2000], [FME 2001], [ZB 2003], thèse de B. Parreaux et C. Darlot.
• Vérification par partie de propriétés LTL. La contribution est une méthode model-checking sur une décomposition du système de transition par le raffinement. La méthode est correcte pour une classe de propriétés LTL incluant les vivacités leadsto et until. Voir publications [IFM 99], [IFM 2000], [TSI 2001], thèse de P.A. Masson.
• Vérification de propriétés LTL sous hypothèses d'équité. La contribution est une définition du raffinement sous équité et une adaptation de l'algorithme de model-checking fondé sur les automates de Büchi pour l'appliquer sans coder les hypothèses d'équité dans l'automate afin d'en réduire la taille. Voir publications [AFADL 2001], [ZB 2002], thèse de S. Chouali.

Je participe également à trois autres activités :

• ACI Sécurité Informatique GECCOO
• Raffinement de systèmes temps-réels. thèse de Emilie Oudot. Voir [AFADL 2003a], [RTS 2004].
• Génération de tests à partir de Politique de Sécurité, projets VALIAS et POSE. Thèse de F. Lebeau, thèse en cours de R. Tissot....:

Jacques JULLIAND Enseignement

Professeur d'informatique à l'UFR Sciences et Techniques de l'Université de Franche-comté. J'y enseigne:

• Sémantique et preuve
  en licence d'informatique et licence d'informatique à distance (cours Logique de Hoare - TD)
• Spécifier pour vérifier
  en Master Informatique 2ème année(cours - TD - TP) : raffinement, logiques temporelles, model-checking
• Automates finis et infinis
  en Master Informatique 2ème année (cours) : produit d'automates, automates de Büchi, automates temporisés
• Compilation
  en Master informatique 1ère année (TD - TP) : analyse syntaxique, sémantiques, génération de code
• Génie Logiciel
  en Master informatique 1ère année (cours) : Modélisation et preuve en B

J'ai enseigné :

• Architecture des machines parallèles en DESS
• Programmation parallèle en DESS
• Algorithmique et programmation en DUT Informatique, DEUG STPI et licence Informatique
• Système en MST Automatique, Electronique et Informatique Industrielle

Jacques JULLIAND Publications depuis 1998

• Articles en revues avec comité de lecture
• Communications internationales avec comité de programme et actes
• Communications nationales avec comité de programme et actes

Articles en revues avec comité de lecture :

• [TSI 99] J. Julliand, F. Bellegarde, B. Parreaux, De l'expression des besoins à l'expression formelle des propriétés dynamiques, TSI, Hermès, vol 18, n°7, 1999.
• [TSI 2001] Julliand J., Masson P-A., Mountassir H. - Vérification par model-checking modulaire des propriétés dynamiques introduites en B. A paraître dans TSI en 2001.
• [TECS 2005] S. Chouali, J. Julliand, P.-A. Masson, and F. Bellegarde. PLTL Partitionned Model-Checking for Reactive Systems under Fairness Assumptions. ACM Transactions on Embedded Computing Systems (TECS), 4(2):267--301, May 2005.

Communications internationales avec comité de programme et actes :

• [B 98] [Julliand J., Legeard B., Parreaux B., Tatibouet B. - Specification of an integrated circuits card protocol application using B and Linear Temporal Logic, 2nd Conference on the B method, LNCS 1393, p. 273-282, Montpellier, France, Avril 1998.
• [IFM 99] Julliand J., Masson P.A., Mountassir H. - Modular verification of dynamic properties for reactive systems. Proc. of the First International Workshop on Integrated Formal Methods, IFM'99, Springer-Verlag, Ed. K Araki, A. Galloway, and K. Taguchi, p. 89-108, York, Grande-Bretagne, 28-29 juin 1999.
• [FM 99] Bellegarde F., Julliand J., Mountassir H. - Model-Based Verification through Refinement of Finite B Event Systems, congrès Formal Method'99, B User Group Meeting, CDROM publication, Toulouse, septembre 1999.
• [FASE 2000] Bellegarde F., Julliand J., Kouchnarenko O. - Ready-simulation is not Ready to Express a Modular Refinement Relation, Fondamental Aspects of Software Engineering 2000, FASE'2000, LNCS 1783, p. 266-283, Springer-Verlag, Berlin, mars 2000.
• [ZB 2000] Bellegarde F., Darlot C., Julliand J., Kouchnarenko O. - Reformulate dynamic properties during refinement and forget variants and loop invariants, ZB2000, LNCS 1878, p. 230-249, York, UK, Août 2000.
• [IFM 2000] J. Julliand, P-A. Masson, H. Mountassir, "Modular verification for a class of PLTL properties".  International Workshop on Integrated Formal Methods,  IFM'2000, LNCS 1945, p. 398-419, Dagstuhl, Saarland, Germany, (1-3 Novembre 2000).
• [FME 2001] F. Bellegarde, C. Darlot, J. Julliand, O. Kouchnarenko , "Reformulation: a way to combine dynamic properties and B refinement", International Symposium Formal Methods Europe 2001, FME 2001, LNCS 2021; , p. 2-19 , Berlin, 12-16 Mars 2001.
• [ZB 2002a] F. Bellegarde, S. Chouali, J. Julliand, "Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions"., Conférence ZB2002, LNCS 2272, p. 477-496, Grenoble, 23-25 janvier 2002.
• [ZB 2002b] F. Bellegarde, J. Julliand, O. Kouchnarenko, "Introducing Component Event Systems Synchronized Parallel Composition in B". Conférence ZB2002, LNCS 2272, p. 436-457, Grenoble, 23-25 janvier 2002.
• [ZB 2003] C. Darlot, J. Julliand, O. Kouchnarenko, "Refinement Preserves PLTL Properties". ZB'03 : Formal Specification and Development in Z and B. Third International Conference of B and Z Users, LNCS n° 2651, p. 408-420, Turku, Finland, (juin 2003).
• [FACS 2005] F. Bellegarde, J. Julliand, H. Mountassir, and E. Oudot. On the contribution of a tau-simulation in the incremental modeling of timed systems. In FACS'05, 2nd Int. Workshop on Formal Aspects of Components Software, volume 160 of Electronic Notes in Theoretical Computer Science, Macao, Macao, pages 97--111, October 2005. Elsevier.
• [MEMOCODE 2005] F. Bellegarde, S. Chouali, and J. Julliand. Refinement Verification of Fair Transition Systems can Contribute to PLTL Model Checking. In Third ACM-IEEE Int. Conf. on Formal Methods and Models for Codesign (MEMOCODE'2005), Verona, Italy, pages 167--176, July 2005. IEEE computer society. Note: ISBN 0-7803-9227-2.
• [eSmart 2006] F. Bouquet, F. Celletti, G. Debois, A. De Lavernette, E. Jaffuel, J. Julliand, B. Legeard, J. Lidoine, J.-C. Plessis, and P.-A. Masson. Model-Based Security Testing, Application to a Smart Card Identity Applet. In eSmart 2006, 7th Int. Conf. on Smart Cards, Sophia-Antipolis, France, September 2006.
• [FATES 2006] F. Bouquet, F. Dadeau, J. Groslambert, and J. Julliand. Safety Property Driven Test Generation from JML Specifications. In K. Havelund, M. Garcia, G. Rosu, and B. Wolff, editors, FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification, volume 4262 of LNCS, Seattle, WA, USA, pages 225--239, August 2006. Springer.
• [SAVCB 2006] F. Bellegarde, J. Julliand, H. Mountassir, and E. Oudot. Experiments in the use of tau-simulations for the components-verification of real-time systems. In SAVCBS'06, Specification and Verification of Component-Based Systems, Portland, Oregon, USA, pages 33--40, November 2006.
• [SAVCB 2006] J. Groslambert, J. Julliand, and O. Kouchnarenko. JML-based Verification of Liveness Properties on a Class. In SAVCBS'06, Specification and Verification of Component-Based Systems, Portland, Oregon, USA, pages 41--48, November 2006.

Communications nationales avec comité de programme et actes :

• [AFADL 98] [Julliand J., Bellegarde F. - Extension des spécifications B par de la Logique Temporelle Linéaire pour décrire des propriétés dynamiques de systèmes réactifs, journées AFADL, "Approches Formelles d'Aide au Développement de Logiciels", Poitiers, Septembre 1998.
• [AFADL 2000] Mountassir H., Bellegarde F., Julliand J., Masson P-A. - Coopération entre preuve et model-checking pour vérifier des propriétés LTL. Journées AFADL, "Approches Formelles d'Aide au Développement de Logiciels", p. 127-141, Grenoble, France, janvier 2000.
  
• [AFADL 2003a] A. Hammad, J. Julliand, H. Mountassir, D. Okalas - Expression en B et raffinement des systèmes réactifs temps réel,.Congrès AFADL'03, Approches Formelles dans l'Assistance au Développement de Logiciels, p. 211-225, Rennes, (15-17 janvier 2003).
• [AFADL 2003b] S. Chouali, J. Julliand, - Model Checking des propriétés dynamiques sous hypothèses d'équité exploitant le raffinement. Congrès AFADL'03, Approches Formelles dans l'Assistance au Développement de Logiciels, p. 277-291, Rennes, (15-17 janvier 2003).
• [RTS 2004] A. Hammad, J. Julliand, H. Mountassir, M. Al Achhab, "Conception et Vérification de systèmes temps réels par raffinement". Congrès RTS 2004, à paraître, Paris.

Pour toute remarque sur cette page, écrire à Jacques Julliand.
Dernière mise à jour le 22 décembre 2006

La formation au L.I.F.C. La recherche au L.I.F.C. Retour à la Home Page L.I.F.C.