Université Catholique of Louvain (BELGIUM)
Automated generation of translators and checking of program transformations.
CADP (Construction and Analysis of Distributed Processes)
In the domain of space-mission planning, a family of languages is used
to describe the control and operation of spacecrafts. As the cost of
developping a dedicated translator for any pair of languages is
prohibitive, a product-line approach is proposed. This approach
exploits the fact that such a family of languages shares a lot of
commonalities to propose a generic to build translators for any pair
of languages in the family. Each translator is defined by a several
program transformations. Moreover, a verification technique to check
the correctness of a program translation is proposed.
The correctness-check of a program translation consists of four steps. First, for both programs (the original one and the translated one) a CFG (Control-Flow Graph) representation is constructed. Second, both CFGs are encoded as LTSs (Labeled Transition Systems). Third, the LTSs are compared with respect to observational equivalence (weak bisimulation) using BISIMULATOR. If the programs are not equivalent, the counter-example is mapped back to the CFG and the source program.
The author reports that:
Diego Antonio Ordonez Camacho.
A Product-Line for Families of Program Translators: A Grammar-Based
Approach. PhD thesis, Université Catholique de Louvain, Belgium,
Available on-line at: https://dial.uclouvain.be/pr/boreal/object/boreal:33289
or from the CADP Web site in PDF or PostScript
Diego Ordóñez Camacho
Pôle d'Ingénierie Informatique
Institute for Information and Communication Technologies, Electronics and Applied Mathematics
Université catholique de Louvain
Place Sainte-Barbe, 2
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|