A simulator for embedded systems is based on a kernel which implements the runtime of a model of the CPU (ARM, PowerPC or MIPS) on which the embedded system is built. Given a machine language program for the considered CPU, this runtime loads a data structure representing the instructions in the program, and execute them on the model of the CPU, each instruction being represented by a particular piece of code. C is probably the best language to express a CPU model both easily and efficiently. We are especialy interested in the simulation of ARM and PowerPC machine code. Our goal is to develop a simulator, SIMSOC, which kernel and CPU model are all certified in Coq for both ARM and PowerPC.

This project is quite innovative: no certified simulator exists on the market and we are not aware of any similar project. When completed, we shall have at our disposal a certified simulator for both ARM and PowerPC. For practical use, the kernel will have to be complemented with input outputs generating traces at run-time for the user executing a particular binary code on the simulator.

Given an abstract processor model, the simulator’s kernel is made of three main components: a reader-loader of the bit machine code described in the ELF standard; a decoder of each machine instruction; an engine made of a set of C functions interpreting the machine instructions w.r.t. the processor model. We shall assume an abstract processor model.

The reader-loader transforms the input string into a data structure representing the machine code stored in the memory model from some given location specified in the string. The reader-loader needs to decode each instruction present in the input string: PowerPC, MIPS. This task is achieved by the decoder. Decoding a sequence of bits representing an intruction of the machine language is actually a cascade of two switches in practice, the first identifying the instruction class, the second the particular instruction in the class. As a consequence, a Caml decoder can be generated from a description of the syntatic format of the instructions.

Task 1: write a certified Caml reader-loader.
Task 2: write a certified Caml decoder-generator taking as input a description of the machine instructions syntax.

The same idea can be used to generate the C code associated with each binary instruction. The instructions of the machine language are based on a few basic operations, and all instructions in a given class are very similar to each other. This should allow to generate these functions -at least most of them- by a CamL program taking as input an SOS description of the meaning of the instructions of the machine language.

Task 3: write a certified Caml engine generator taking as input an SOS description of the machine instructions semantics. This assumes an SOS based language to specify the meaning of ARM/PowerPC instruction machine instructions.

The goal of the internship is to design a network protocol for the communication between a graphical user interface running on a PC and a simulator running on a remote machine.

This network protocol must:

• support bi-directional communications.
• support multiplexing of control flows on the communication channel. It may be that the simulator has multiple components that can be controlled individually.
• be evolutive such that future versions of the protocol can include new features while existing applications continue to run using the old version.

The student must first specify the protocol, as a TCP/IP based protocol, then implement it as a library in C or C++ (the student can choose). The library shall be tested with unit test programs to ensure proper function and check for potential regressions in the future.

The student will need to communicate with other team members who implement the man machine interface and the simulator, and write a documentation in english on how to use the library.

This is at least a 5 months project, preferably 6 months.

The goal of the project is to investigate into the simulator developed in the FORMES project the possibility to simulate hardware components using parallell simultaneous simulation models to run on multi-processor simulation machines. This means that either the current scheduler must be extended to support parallell components, or alternatively that a new framework should be developed inherently supporting concurrency of simulation models. Both options are open in this preliminary phase.

Many powerful termination criteria have been developed for rewrite rules based programs. Rewriting is a fundamental notion that is also of practical interest since programs in other programming paradigms can be encoded by using rewrite systems. Currently, CoLoR can handle rewrite systems only. We propose various subjects to extend CoLoR with other important termination techniques and to other programming paradigms. Find more details here.

Define a translation of membership equational logic to the Calculus of Inductive Constructions, in which sorts from equational logic are translated to inductive types. Note that some defined symbols like tail on lists are total on a subsort (of lists): since subsorts do not exist in the Calculus of Inductive Constructions, they must take in the translation a proof that the input is non-empty as a new argument. Define and implement a decision procedure with certificates for confluent and terminating specifications in MEL. Further, define Higher-Order Membership Equational Logic so as to retain the nice properties of this logic: existence of an initial algebra, efficient execution schema, etc.