Formal Methods and Programming Language Translation – Translating CCS (Calculus of Communicating Systems) into CSP (Communicating Sequential Processes)
By Gérald Ekembe Ngondi
Bio : I have a BEng from the National School of Post & Telecommunications in Yaounde, an MSc and a PhD from the University of York, UK. My research interests include the semantics of programming languages, the unification of formal methods, the verification of programs, and the analysis of concurrent and distributed systems. I have notably extended the language CSP (Communicating Sequential Processes) with both channel mobility and process migration, in collaboration with Prof. Jim Woodcock, and provided the first correct translation of CCS (Calculus of Communicating Systems) into CSP, in collaboration with Dr. Andrew Butterfield and Dr. Vasileios Koutavas.
Absract : This presentation aims to introduce Formal Methods and their application to the problem of translation between two programming languages. Formal methods denote the collection of mathematical techniques used for the analysis of computer systems. Typically, a formal method is composed of a formal specification language (or simply formal language), which determines the syntax of programs to be analysed. Different methods propose different language syntax, all of which often serve to represent the same program. A similar situation occurs with programming languages and raises the question of the equivalence between programs. I will discuss the problem of translation between two prominent formal languages, CCS (Calculus of Communicating Systems) into CSP (Communicating Sequential Processes). CCS was pioneered by Prof. Robin Milner (Turing Award 1991), may he rest in peace, and CSP by Prof. Tony Hoare (Turing Award 1980). Both CCS and CSP allow analysing concurrent programs and were considered distinct for the past 40 years, in spite of their similarities. I will notably show how different design decisions affect the degree of correctness of the translation function.
Modéliser et tester des systèmes évolutifs
Par Omer Nguena Timo
Bio : Omer Nguena Timo, Ph.D. est professeur agrégé à l’Université du Québec en Outaouais, codirecteur du module de l’informatique et président d’un comité de sélection des bourses du conseil de recherches en sciences naturelles et en génie du Canada (CRSNG). Dans ses travaux de recherche, il développe des méthodes de test et de vérification à base de la logique et des modèles formels pour construire des systèmes informatisés évolutifs fiables et sécurisés. Il a notamment travaillé en France et au Québec pour accroître l’innovation dans des industries des milieux de l’automobile, de l’aéronautique et des télécommunications. Omer est Diplômé au doctorat en informatique de l’Université Bordeaux 1 – France et d’une maîtrise en informatique de l’Université de Yaoundé 1 – Cameroun.
L’Internet des Objets (Isolés) par Satellite (SatIoT)
Par Didier Donsez
Bio : Didier Donsez est Professeur des Universités en informatique à l’Université Grenoble Alpes (Grenoble, France) depuis 2007. Il est actuellement en délégation au CNRS. Il a été Maître de Conférences en informatique à l’Université de Valenciennes (France) de 1996 à 2001, puis à l’Université Joseph Fourier (Grenoble, France) de 2001 à 2007. Il a obtenu un doctorat en informatique (1994) à l’Université Paris VI : Pierre et Marie Curie et une HDR (Habilitation à Diriger des Recherches) en informatique (2006) à l’Université Joseph Fourier. Son laboratoire de recherche est le LIG (Laboratoire d’Informatique de Grenoble) [https://www.liglab.fr], au sein de l’équipe ERODS [http://erods.liglab.fr]. Il enseigne au département d’informatique de Polytech Grenoble (école d’ingénieurs). Ses domaines de recherche portent sur les systèmes distribués, les intergiciels et le génie logiciel pour l’internet des objets (IoT) depuis 20 ans. Ses sujets actuels incluent LPGAN, SatIoT et l’intelligence artificielle à la périphérie des réseaux (extreme edge). Il est le promoteur du projet Thingsat, un véhicule de recherche en orbite pour l’évaluation de la modulation LoRa© dans les applications SatIoT. Il s’intéresse à l’usage de l’IoT dans les sujets environnementaux et sociétaux. Il participe à plusieurs projets logiciels open-source. Pages web : http://www.linkedin.com/in/didierdonsez, http://membres-liglab.imag.fr/donsez/, https://gricad-gitlab.univ-grenoble-alpes.fr/thingsat/public/