Curriculum vitæ

Samuel Colin

Table des matières

1  Informations

Nom
Samuel Colin
Mail
scolin(at)hivernal(dot)org
LinkedIn
https://www.linkedin.com/in/sjdcolin
Divers
Nationalité française
Titulaire du permis B
3ème dan de Kyudo

2  Expériences

01/2017–
Ingénieur sûreté et cybersécurité, logicielle et système
Pour Autoliv→Veoneer: Aide à la mise en place de l’ISO26262 pour les plateformes et projets d’ECU devant accueillir des fonctions d’ADAS (Advanced Driver Assistance Systems), pour le système et pour le logiciel. Support pour la mise en place de processus orientés Cybersécurité pour tous les projets en général.
04/2016–01/2017
Ingénieur sûreté logicielle
Mise en œuvre pour la RATP de la méthode (preuve d’équivalence spécification/programme C) développée précédemment sur le code C du logiciel bord d’OCTYS L5.
11/2015–04/2016
Ingénieur sûreté logicielle
Étude pour la RATP de faisabilité de la preuve d’équivalence de programmes C avec leur spécification, avec l’aide de l’atelier de preuve RATP basé sur HLL+tecla. Définition de règles de transformation des programmes C pour rendre la preuve possible. Conception d’outils pour réaliser ces transformations et rédaction de la documentation associée.
09/2015–11/2015
Ingénieur sûreté logicielle
Validation pour la RATP des logiciels de base développés et déployés sur la ligne L13. Traçabilité des exigences de sécurité logicielle, suivi des corrections demandées à l’industriel
09/2014–08/2015
Ingénieur sûreté logicielle
Développement et mise en œuvre pour Autoliv d’un (prototype d’)outil d’analyse statique de code permettant de détecter et d’instruire les interférences entre logiciels de niveaux d’ASIL différents dans le contexte d’une architecture AUTOSAR.
01/2014–12/2014
Ingénieur cybersécurité logicielle
Développement d’un outil d’analyse de code C pour la rechercher de vulnérabilités (CWE). Développement de la base de tests associée ( 90000 tests). L’outil est basé sur la souche «open-source» Frama-C du CEA LIST.
11/2012–12/2013
Ingénieur sûreté logicielle
Constitution d’un programme de formation pour la RATP constitué d’une introduction aux méthodes formelles – pilotage, rédaction et relecture des documents produits
11/2011–12/2013
Ingénieur sécurité système
Analyses de sécurité sur les données de la ligne 13 pour Thales RSS.
07/2013
Ingénieur cybersécurité logicielle
Constitution d’une base de tests couvrant les exigences client pour un outil de génération de valideurs XML à partir de schémas XSD décrivant le format autorisé des fichiers XML (pour un outil Thales)
09/2012–10/2012
Ingénieur cybersécurité système
Analyse de sécurité (au sens SSI) d’un composant de communication sans fil embarqué dans un système avionique pour Safran. Utilisation de la méthode EBIOS
06/2012–07/2012
Ingénieur sûreté logicielle
Vérification pour la RATP du pilote automatique embarqué (PAE) de la ligne 1 décrit sous forme de composants B (mise à jour pour 2012 de la version de 2011)
11/2011–05/2012
Ingénieur cybersécurité logicielle
Développement et vérification d’un compilateur de valideurs XML paramétrés par des grammaires décrites au format XSD pour l’ANSSI
07/2010–11/2011
Ingénieur sûreté logicielle
Prestataire à la RATP dans l’équipe AQL
Validation de la partie logicielle écrite en B de pilotage automatique pour la ligne 1 du métro parisien.
07/2010–
Ingénieur en sûreté et sécurité logicielles des systèmes embarqués à SafeRiver
03/2009–08/2009
Contrat UVHC dans le cadre du projet TACOS (http://tacos.loria.fr)
Intégration des travaux sur CSP||B et le composant de localisation
10/2008–02/2009
Période de chômage mise à profit pour travailler sur BiCoax
(cf http://pauillac.inria.fr/pipermail/coq-club/2009/004424.html)
10/2007–09/2008
Post-doctorat Nancy 2/LORIA
Continuation du sujet de l’année précédente
Formalisation de systèmes Multi-Agents situés en collaboration avec l’équipe MAIA du LORIA
10/2006–09/2007
Post-doctorat Nancy 2/LORIA
Sujet : spécification d’adaptateurs sûrs dans une approche composants avec la méthode B
01/2005–08/2006
Demi-ATER à l’UVHC
01/2002–12/2004
Allocataire de recherche dans l’unité de recherche «Évaluation des systèmes de transport automatisés et de leur sécurité» (ESTAS) de l’institut national de recherche sur les transports et leur sécurité (INRETS)
04/2001–09/2001
Stage de DEA
Méthode B et temps réel : étude de l’intégration du calcul des durées
05/2000–07/2000
Stage de maîtrise
Implantation d’une librairie OCaml pour le calcul des substitutions B
Participation au développement de la plateforme logicielle Brillant (anciennement BCaml)

3  Formation

3.1  01/2002–10/2006 : Thèse de doctorat

Titre
Contribution à l’intégration de temporalité au formalisme B : Utilisation du calcul des durées en tant que sémantique temporelle pour B
Date de soutenance
3 octobre 2006
École doctorale
École doctorale de l’Université de Valenciennes et du Hainaut-Cambrésis (UVHC)
Discipline
Informatique
Spécialité
Automatique et Informatique des Systèmes Industriels et Humains
Jury :
Président
Pascal Yim, professeur à l’École Centrale de Lille
Rapporteur
Didier Bert, chargé de recherche CNRS au LSR-IMAG (Grenoble)
Rapporteur
Hassan Mountassir, professeur à l’université de Franche-Comté (Besançon)
Examinateur
Arnaud Fréville, directeur de thèse, professeur à l’UVHC
Examinateur
Vincent Poirriez, co-directeur, maître de conférences à l’UVHC
Examinateur
Georges Mariano, co-directeur, chargé de recherches à l’INRETS
Mention
Très honorable

3.2  2000–2001 : DEA

Intitulé
DEA Programmation : Sémantique, Preuves et Langages
Lieu
Université Paris 7
Modules suivis
termes en logique du premier ordre et systèmes de réécriture, lambda-calcul, preuves constructives, sémantique des programmes séquentiels et concurrents, typage et programmation, langages synchrones, sous-typage et langages à objets, concurrence et mobilité, techniques d’analyse par interprétation abstraite, vérification de systèmes infinis.
Stage
«Méthode B et temps-réel : étude de l’intégration du calcul des durées» (responsable : Vincent Poirriez)
Mention
Bien

3.3  1999–2000 : Maîtrise

Intitulé
Maîtrise d’informatique
Lieu
UVHC
Modules suivis
intelligence artificielle, réseaux et architectures distribuées, systèmes répartis, architectures parallèles, algorithmique et programmation parallèle, graphes, bases de données, optimisation combinatoire et heuristiques, génie logiciel, programmation orientée objet.
Mention
Très bien

3.4  1998–1999 : Licence

Intitulé
Licence d’informatique
Lieu
UVHC
Modules suivis
algorithmique, méthodologie de programmation, systèmes d’exploitation, architecture des ordinateurs, langages et compilation, recherche opérationnelle.
Mention
Très bien

3.5  1996–1998 : DEUG

Intitulé
DEUG Mathématiques, informatique et applications aux sciences
Lieu
UVHC
Mention
Bien

3.6  1996 : Baccalauréaut

Intitulé
série S (scientifique)
Lieu
Lycée Henri Wallon, Valenciennes
Mention
Mention Bien

4  Langues

Français
langue maternelle. Orthographe et grammaire soignées
Anglais
lu, écrit, parlé. Anglais technique courant
Allemand
niveau scolaire
Roumain
notions
Japonais
notions

5  Compétences

Ci-après se trouvent les compétences que j’utilise au jour le jour ou que j’ai eu l’occasion de pratiquer en profondeur.

Formalismes
Méthode B, event-B, Coq
Prouveurs
B4Free, Coq
Langages
OCaml, C, PHP
Documentation
XHTML, XML, CSS, TEX/LATEX
Systèmes de gestion de version
CVS, Subversion, Darcs, git
Infographie
Blender, Gimp, Inkscape
Systèmes d’exploitation
Linux (Debian), scripting et administration système Unix

6  Enseignement

Les heures indiquées dans cette section sont les heures effectives et non «équivalent TD». Le total des heures de TD s’élève à 86 et celui des heures de TP à 200 (soit 133H ETD), qui font 286 heures d’enseignement, ou 219 heures équivalent TD.

6.1  Spécification formelle et sûreté logicielle

Niveau
Master 1/IUP 3 d’informatique
Description
étude de la problématique de sûreté des logiciels, avec la méthode B. Les outils utilisés changent selon les années et sont spécifiés ci-dessous.
Détail des heures

6.2  Méthodologie de programmation

Niveau
Licence 3/IUP 2 d’informatique
Description
introduction à la programmation fonctionnelle, récursivité, programmation modulaire, programmation objet, programmation concurrente, avec le langage OCaml
Détail des heures

6.3  Bases de la complexité et algorithmique

Niveau
Licence 3/IUP 2 d’informatique
Description
étude des complexités temporelle et spatiale des algorithmes, avec les langages C et OCaml
Détail des heures

6.4  Langages et grammaires

Niveau
Licence 3/IUP 2 d’informatique
Description
langages réguliers, automates, grammaires régulières. Outils utilisés : grep, sed. Langage utilisé : OCaml
Détail des heures

6.5  Programmation avec Pascal

Niveau
DEUG Sciences de la Matière
Description
apprentissage de la programmation avec le langage Pascal
Détail des heures

7  Encadrement d’étudiants

Les formations où je suis intervenu proposent chaque année des projets que les étudiants doivent réaliser eux-mêmes. Les sujets sont proposés par les enseignants qui en assurent l’encadrement. Dans la grille horaire, cela correspond à une demi-journée libérée chaque semaine pour que les étudiants puissent travailler sur leur projet, et éventuellement faire un point régulier avec leur encadrant. Le projet est validé par la production d’un rapport, souvent d’un programme, et une soutenance en fin d’année.

L’encadrement correspond à 1,5H équivalent TD par étudiant encadré et par semestre.

2004/2005

Niveau
Licence 3
Sujet
OCaml Pong
Description
Mise en oeuvre d’un jeu de type «Pong» en 3 dimensions, en utilisant OCaml et OpenGL

2002/2003

Niveau
Maîtrise
Sujet
Vérification statique de projets B
Description
Vérification statiques du respect des contraintes de modularité dans un projet B

8  Charges collectives

2009–aujourd’hui
Traduction française de la «Not so short introduction to LATEX 2є» (http://hivernal.org/static/computing/doc/lshort-fr.fr.html)
2007–2008
Dans l’équipe DEDALE du LORIA
2002–aujourd’hui
Coordination et développement au sein de la plateforme Brillant (https://gna.org/projects/brillant) d’outils pour la méthode B :
2002–aujourd’hui
Coordination et développement pour le projet Sandbox-OCaml (https://gna.org/projects/sb-ocaml/) de mise en commun de tutoriels et de projets OCaml laissés à l’abandon
2003–2004
Membre élu du collège doctorants pour le conseil d’administration de l’institut des sciences et techniques de Valenciennes (ISTV)
2002–2005
Aide à l’administration système dans l’unité de recherche ESTAS de l’INRETS (réseau de cinq machines sous Linux, utilisées pour le stockage et le calcul intensif, numérique et symbolique)

9  Personnes à contacter

Les personnes suivantes, avec lesquelles j’ai travaillé par le passé, peuvent être contactées afin de donner leur opinion sur la qualité de mon travail. Les entrées sont par ordre décroissant de durée de collaboration:

Pr Vincent Poirriez
mailto:vincent.poirriez@univ-valenciennes.fr. Tel: +33 3 27 51 19 53
Dr Georges Mariano
mailto:georges.mariano@inrets.fr. Tel: +33 3 20 43 84 06
MdC Arnaud Lanoix
mailto:arnaud.lanoix@univ-nantes.fr. Tel: +33 2 40 30 60 56
Pr Jeanine Souquières
mailto:jeanine.souquieres@loria.fr. Tel: +33 3 83 59 20 12
Pr Olga Kouchnarenko
mailto:kouchna@lifc.univ-fcomte.fr. Tel: +33 3 81 66 65 24
MdC Olivier Simonin
mailto:olivier.simonin@loria.fr. Tel: +33 3 83 59 30 43
Pr François Charpillet
mailto:francois.charpillet@loria.fr. Tel: +33 3 83 59 20 81

10  Publications

Les auteurs des papiers sont indiqués par ordre de contribution. Je préciserai, lorsque je ne suis pas premier auteur, mon rôle dans chaque papier que j’ai co-signé. Je résume certains de mes articles lorsque j’estime que c’est pertinent. Les articles ou rapports qui présentent mes travaux les plus récents sont [11], [21], [3], [2], [9], [20], [1] et [24]. Ils sont tous disponibles, ou leurs versions en tant que rapports de recherche, via http://hivernal.org/static/about/.

10.1  Revues nationales avec comité

L’article [1] est une synthèse des travaux de l’équipe DEDALE sur la notion d’adaptateur dans le cadre de l’interopérabilité et de la fiabilité de composants fournis. Il reprend notamment l’adaptation du modèle de données décrit au workshop international FESCA [10] en l’intégrant dans la démarche plus générale d’adaptation de composants. Il s’agit d’une version étendue et plus détaillée de l’article [7].

10.2  Conférences internationales avec comité

[3] décrit BiCoax, l’outil de preuve basé sur un plongement léger de B en Coq. Il est destiné plutôt à un public familier de B et décrit les choix d’implantation, les résultats théoriques (avec quelques erreurs mineures découvertes et documentées) ainsi qu’un retour sur expérience d’une mise en application en tant qu’outil de preuve automatique et en tant qu’interface de preuve sur des projets B simples. Par rapport à [24], cet article ajoute des remarques supplémentaires concernant les entiers naturels de B et constate l’utilisabilité de l’outil sur des projets B simples.

L’article [2] présente le problème du platooning sous un angle architectural : comment intégrer dans le même modèle la vue des composants d’un véhicule et la vue du système de véhicules complet ? Nous utilisons pour ce faire CSP||B pour assurer que les communications entre composants et entre véhicules vérifient de bonnes propriétés de non-divergence et d’absence d’interblocage.

L’article [5] présente la plateforme BRILLANT de développement pour B citée en section 8 et notre approche ouverte et intégratrice dans le cadre de cette plateforme.

L’article [6] décrit une étude de cas de passage à niveau exprimée en UML et validée avec la méthode B. Cette étude de cas comporte des contraintes temporelles, mon rôle dans ce papier a été de vérifier la cohérence des contraintes temporelles du modèle et de mentionner quels formalismes temporisés compatibles avec la méthode B peuvent être utilisés pour simplifier l’expression et la validation de l’étude de cas.

L’article [4] correspond à un extrait de mes travaux de thèse, où je présente une sémantique en calcul des durées, une logique temporelle, pour la méthode B.

10.3  Conférences nationales avec comité

L’article [7] est l’un des articles pressentis pour apparaître dans la revue “Technique et Science informatiques”, cf. [1] en section 10.1.

L’article [8] décrit une mise en œuvre d’un prouveur de logique du premier ordre en théorie des ensembles. Ce prouveur est basé sur une bibliothèque pour un prouveur appelé PhoX. Mon rôle dans cet article se situe au niveau de l’outil, c’est-à-dire que j’ai complété ce qu’il manquait à la plateforme logicielle citée pour obtenir des formules à valider via le prouveur. Mon autre contribution à ce papier consiste en des choix techniques concernant la bibliothèque elle-même, avec pour objectif de simplifier et accélérer les preuves.

10.4  Workshops internationaux avec comité

L’article [11] présente sommairement les spécificités et le contexte de la plateforme BRILLANT (cf sections 10.2 et 8), ainsi que sa récente évolution dans le choix de l’assistant de preuves retenu.

L’article [9] est une évolution de [2]. Il montre un meilleur usage des outils pratiques et théoriques utilisés. En particulier nous avons utilisé des théorèmes existants de CSP||B pour remplacer un composant par plusieurs autres et démontrer que le protocole était préservé. Il s’agit d’un raffinement de protocole, pour lequel les théorèmes mentionnés ci-avant n’ont pas été conçus a priori pour.

L’article [10] montre comment réaliser une connexion fiable entre composants proches via un adaptateur. Les composants doivent avoir des fonctionnalités proches et des modèles de données éventuellement différents. L’adaptation se fait via un raffinement B qui montre comment exprimer l’interface requise d’un composant à l’aide de l’interface fournie de l’autre composant. De par la technique utilisée, l’adaptation résultante est digne de confiance.

L’article [12] traite des diverses possibilités d’implémentation d’une logique modale dans un prouveur générique, en séparant l’argumentation sur la dichotomie entre plongement léger (seuls les éléments manquants de la logique sont ajoutés) et plongement profond (la logique et ses règles dans leur ensemble sont réimplantées dans le prouveur).

10.5  Communications nationales

[14] est une ancienne présentation faite aux journées B du GDR ALP. Elle traite de la faisabilité d’utiliser le calcul des durées avec B.

10.6  Ouvrages

[13] est une traduction en français de la fameuse «Not so short introduction to LATEX 2є». La dernière traduction librement diffusée était en effet très obsolète : c’était donc l’opportunité de remettre à jour cette traduction.

10.7  Séminaires

[15] est une présentation qui résume l’état de l’art sur la notion de composition en B. C’est à ce titre de résumé informatif de l’état de l’art que je la cite ici.

10.8  Autres publications

[21] continue à la suite de [2] et [9]. Il s’agit de réintégrer le composant de localisation développé en B par d’autres équipes au sein du projet TACOS. Cette réintégration pose le problème d’architecture illégale en CSP||B car un partage entre sous-composants apparaît. Nous proposons donc une vérification additionnelle basée sur la modularité de B ainsi qu’une simplification de certains critères de vérification CSP||B basée sur cette connaissance architecturale. Sur la base des travaux sur CSP||B et ce travail nous conjecturons quels ajustements seraient nécessaire pour être capable de prendre en compte d’autres patrons d’architecture.

[24] est dérivé d’une tentative de publication aux JFLA présentant une implémentation en Coq d’un plongement léger de la théorie ensembliste de B. L’outil correspondant, appelé «BiCoax», est fidèle au BBook, ce qui a permis la découverte d’erreurs mineures. Son avancement le rend également utilisable en tant qu’outil de preuve pour B. Ce document n’est plus à jour étant donné que l’implémentation a beaucoup avancé.

[22] correspond à la version de soumission de [2]. Il me semble important ici de préciser que [28, 19, 20] avaient été soumis à des revues et conférences, et retournés à chaque fois avec de bons commentaires, mais refusés car jugés trop hors-sujet.

[19] est une prolongation de [28] qui présente beaucoup plus en détail les modèles B, et [20] étend encore cette présentation en discutant en profondeur les preuves effectuées et ce qu’elles signifient par rapport au modèle du «platooning».

L’article [28] traite de la formalisation d’un système multi-agents situé de véhicules devant se déplacer en convoi, appelé «platooning». Ma contribution à cet article consiste en la modélisation en B «classique» et la preuve des modèles B obtenus. J’ai également contribué à la rédaction de la partie correspondante et participé à la présentation de l’architecture du modèle B en général. Ce travail présente en outre des patterns de modèles B pour le modèle Influence/Réaction du monde des Multi-Agents.

L’article [27] a été soumis en Avril 2006 à la revue SoSym (Software and System Modeling) mais refusé au final, nous avons donc décidé d’en faire un rapport de recherche/documentation pour la plateforme BRILLANT. Il est basé sur un article mentionné en section 10.2, et je suis intervenu sur des parties dont le premier auteur n’était pas familier.

11  Bibliographie

Revues nationales avec comité

[1]
Arnaud Lanoix, Samuel Colin, and Jeanine Souquières. Développement formel par composants : assemblage et vérification à l’aide de B. Technique et Science Informatiques (TSI), 27(8):1007–1032, 2008. numéro spécial AFADL07.

Conférences internationales avec comité

[2]
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, and Jeanine Souquières. Towards validating a platoon of cristal vehicles using CSP||B. In J. Meseguer and G. Rosu, editors, 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), volume 5140 of LNCS, pages 139–144. Springer-Verlag, July 2008.
[3]
Samuel Colin and Georges Mariano. BiCoax, a proof tool traceable to the BBook. In From Research to Teaching Formal Methods - The B Method (TFM B’2009), June 2009.
[4]
Samuel Colin, Georges Mariano, and Vincent Poirriez. Duration calculus: A real-time semantic for B. In First International Colloquium on Theoretical Aspects of Computing, Guiyang, China, September 2004. UNU-IIST. selectivity : 36/111.
[5]
Samuel Colin, Dorian Petit, Jérôme Rocheteau, Rafaël Marcano, Georges Mariano, and Vincent Poirriez. BRILLANT : An open source and XML-based platform for rigourous software development. In SEFM (Software Engineering and Formal Methods), Koblenz, Germany, September 2005. AGKI (Artificial Intelligence Research Koblenz), IEEE Computer Society Press. selectivity : 40/120.
[6]
Rafaël Marcano, Samuel Colin, and Georges Mariano. A formal framework for UML modelling with timed constraints : Application to railway control systems. In SVERTS: Specification and Validation of UML models for Real Time and Embedded Systems, Lisbon, Portugal, October 2004. (in conjunction with 7th International Conference on the Unified Modeling Language, UML 2004).

Conférences nationales avec comité

[7]
Arnaud Lanoix, Samuel Colin, and Jeanine Souquières. Schémas de développement d’adaptateurs à l’aide de B. In Approches Formelles dans l’Assistance au Développement de Logiciels, pages 91–108, June 2007.
[8]
Jérôme Rocheteau, Samuel Colin, Georges Mariano, and Vincent Poirriez. Évaluation de l’extensibilité de PhoX : B/PhoX un assistant de preuves pour B. In JFLA, pages 139–153, January 2004.

Workshops internationaux avec comité

[9]
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, and Jeanine Souquières. Using CSP||B components: Application to a platoon of vehicles. In Darren Cofer and Alessandro Fantechi, editors, 13th International ERCIM Wokshop on Formal Methods for Industrial Critical Systems (FMICS 2008), volume 5596 of LNCS, pages 103–118. Springer-Verlag, September 2008.
[10]
Samuel Colin, Arnaud Lanoix, and Jeanine Souquières. Trustworthy interface compliancy: data model adaptation. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), Satellite workshop of ETAPS, number 203/7 in ENTCS, pages 23–35. Elsevier, March 2007.
[11]
Samuel Colin, Dorian Petit, Georges Mariano, and Vincent Poirriez. BRILLANT: an open source platform for B. In Workshop on Tool Building in Formal Methods (held in conjunction with ABZ2010), February 2010.
[12]
Samuel Colin, Vincent Poirriez, and Georges Mariano. Thoughts about the implementation of the duration calculus with Coq. In 4th International Workshop on the Implementation of Logics. University of Liverpool, September 2003. Technical report ULCS-03-018.

Ouvrages

[13]
Samuel Colin and Manuel Pégourié-Gonnard. Une courte (?) introduction à LATEX 2є. self-publishing, February 2010. traduit de "The not so short introduction to LATEX 2є" par Tobias Oetiker – ouvrage librement accessible.

Communications nationales

[14]
Samuel Colin. B et le temps réel: Étude de l’intégration du calcul des durées. In Journées du groupe B du GDR ALP, June 2002.

Séminaires

[15]
Samuel Colin. Compositionnalités en B classique et étendu : tour d’horizon. Séminaire dans l’équipe CPR du CEDRIC au CNAM, July 2006.

Divers

[16]
Samuel Colin. Implémentation d’une librairie OCaml pour le calcul des substitutions B. Technical report, INRETS/ESTAS, 20 rue Élisée Reclus, BP 317 – 59666 Villeneuve d’Ascq, 2000.
[17]
Samuel Colin. Méthode B et temps réel : étude de l’intégration du calcul des durées. Mémoire de DEA, Université de Paris VII, 2001.
[18]
Samuel Colin. Contribution à l’intégration de temporalité au formalisme B : utilisation du calcul des durées en tant que sémantique pour B. Thèse de doctorat, Université de Valenciennes et du Hainaut-Cambrésis, October 2006.
[19]
Samuel Colin and Arnaud Lanoix. An experience with a formal modelling of a multi-agent system: the platooning problem. Technical Report hal-00260568, LORIA, December 2007.
[20]
Samuel Colin and Arnaud Lanoix. An experience with a formal modelling of a multi-agent system: the platooning problem. Technical Report hal-00260573, LORIA, January 2008.
[21]
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, and Vincent Poirriez. Bringing state sharing into CSP||B: a B-based approach. Technical report, self-publishing, October 2009.
[22]
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, and Jeanine Souquières. Towards validating a platoon of cristal vehicles using CSP||B. Technical Report hal-00261630, LORIA, March 2008. Submitted to AMAST’08.
[23]
Samuel Colin, Arnaud Lanoix, and Jeanine Souquières. Trustworthy interface compliancy: data model adaptation. Research Report hal-00123884, LORIA, January 2007.
[24]
Samuel Colin and Georges Mariano. Coq, l’alpha et l’omega de la preuve pour B ? Technical report, INRETS, February 2009.
[25]
Samuel Colin, Georges Mariano, and Vincent Poirriez. A natural extension of B substitutions : postconditions. Technical report, LAMIH/ROI, 2004.
[26]
Arnaud Lanoix, Samuel Colin, and Jeanine Souquières. Schémas de développement d’adaptateurs à l’aide de B. Research Report hal-00131340, LORIA, February 2007.
[27]
Dorian Petit, Samuel Colin, Georges Mariano, Vincent Poirriez, Jérôme Rocheteau, and Rafaël Marcano. An open source and XML-based platform for rigourous software development. Technical report, BRILLANT, April 2006.
[28]
Olivier Simonin, Arnaud Lanoix, Samuel Colin, Alexis Scheuer, and François Charpillet. Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems. INRIA Research Report 6304, INRIA, September 2007.
Ce document a été traduit de LATEX par HEVEA