Esterel to SMV

Esterel을 model checker인 SMV의 input으로 변환하면 어떨까 고민하던 중 발견하게 된 논문이 있었다. "Symbolic Anaysis Laboratory" 라는 제목의 논문은 Esterel, ASM, Java 등의 source language로 부터 입력을 받아 SAL이라는 자신의 intermediate langauge로 변환하고 그로 부터 여러가지 theorem prover, model checker, static analyzer의 input으로 변환해주는 translator를 포함하는 system verification의 종합선물세트같은 framework를 소개하고 있었다.

다음주 랩세미나의 주제를 SAL에 대한 survey talk로 정하고 논문을 탐독하던중 Framework의 전체그림에 그려져 있던 Esterel to SAL translator가 실제로 구현되어 있는 건지 아직 개발이 안된건지 궁금해졌고 바로 엉터리 영어를 동원해 메일을 보냈다.

그리고 오늘 아침 답장을 받았다.

Hi Kim,

We had a translator for the Esterel intermediate format EQF. The Esterel Tools have a translator from Esterel to EQF. They changed the intermediate format, and our translator does not work anymore.

Anyway, I think it would be nice to have a translator from Esterel to SAL which does not depends on an external translator. Gerard Berry has a nice paper describing how to translate Esterel to languages like SAL. His paper describes all necessary 'tricks' to implement a translator. However, I guess it would take a couple of months to implement such translator.

Cheers,
Leonardo.

이름부터 멋진 이 친구는 친절하게 답장을 써줘서 참 고마웠다. 결론은 쓸만한 Esterel to SAL translator는 현존하지 않는다는 것이며 Berry의 논문이 힌트가 될 수 있을 것이라는 것!

석사논문 주제로 해볼만 한 일인지 계속 고민해봐야겠다 ...