Interconnecting the ObjectGEODE and CAESAR-ALDEBARAN toolsets

Most of SDL tools, either commercial or academic, propose functionalities related to the code generation and test suites generation or application; this is sometimes combined with some formal analysis capabilities, based on a more or less exhaustive and controlled simulation. But no SDL tools propose more advanced formal verification activities, like the evaluation of temporal logic formula or the use of bisimulation relations to compare SDL specifications or minimize SDL models. This paper presents the interconnection of the formal verification toolbox CAESAR-ALDEBARAN with the commercial toolbox ObjectGEODE. This interconnection allows to extend the formal analysis capabilities of the ObjectGEODE simulator. One part of this connection is done through an API to the internal functions of the simulator, thus allowing to apply the 'on the fly' verification methods of CAESAR-ALDEBARAN.