||Former post-doctoral fellowship at INRIA
Rhône-Alpes, from January 1997 to May 1998. Member of the VASY
team, collaborating with the SIRAC
and SHERPA projects.
During the first years he studied how to apply the formal description technique LOTOS to the specification of operating systems. In this context he contributed to the ESPRIT project "Aphrodite", where he developed a specification of the CHORUS distributed operating system.
He then focused his interest on the improvement of the data type part of LOTOS. He first proposed an extension of LOTOS libraries, then designed and implemented a set of facilities that allow for simpler and more portable data type definitions. In the Euro-Canadian project Eucalyptus, he worked on the integration of several LOTOS-related programs into a user-friendly integrated toolbox. He has also been actively contributing to the ongoing work on enhancements of LOTOS within ISO, promoting a strongly typed functional model for data types. He obtained his Doctorate in Applied Sciences in November 1996 with a thesis entitled "Improving the Specification of Data Types in LOTOS".
Besides this, Charles Pecheur worked on protocol implementation in a UNIX kernel within ESPRIT project BWN, on the design of a tactical simulation program for the Belgian Army and on the formal validation of a multimedia access control protocol within ACTS project OKAPI. He was also responsible for the system and network administration of different kinds of computers in his department.
In January 1997, Charles Pecheur joined the VASY team of INRIA Rhône-Alpes in France. He applied his knowledge of the LOTOS language and tools to the validation of two applications developed in other INRIA projects and Bull, within the DYADE joint venture: a distributed knowledge base and a cluster file system. He also worked on performance improvements for the CAESAR LOTOS compiler.
In May 1998, he moved to the San Francisco Bay area as a research scientist in the Automated Software Engineering Group at NASA Ames Research Center, to take part in the extension of their activities in formal methods and model checking.