Developed Products

Simulink to CSP (methodology and tool support): Plug-in for Matlab/Simulink that automatically translates a (discrete) Simulink diagram into a specification in the process algebra CSP. The model checker FDR2 is used to check properties of such a system. We have used this solution to analyse a system known as Fly-by-Wire provided by Embraer, among other case studies;

Simulink to Prism (methodology and tool support): Plug-in for Matlab/Simulink that automatically translates a Simulink diagram, annotated with failure logic and rates, into a specification in the Markov-based language and tool Prism. The probabilistic model checker Prism is used to check whether certain failure conditions violates their criticalities according to a safety assessment process (in particular the ARP4761);

Sequential to concurrent Java (methodology): We created a methodology based on refactoring laws that takes a sequential Java program as input and transforms it into an equivalent concurrent version able to explore multicore architectures. Some experiments have shown that we can obtain a similar result as a concurrent program made by a human programmer. Our goal is to exploit the benefits of improving legacy code without human interference in the process.