In case of developing safety-critical software, formal methods are stipulated by international standards.
We are performing research on the introduction of formal methods (Event-B, B-method) into actual development processesaccording to the Embedded System development Process Reference (ESPR) to be able to provide the methods for introducing formal methods into each process and the technologies for securing consistency with development documents.

Tool image

Event-B
(Method specialized for upper processes)

RODIN platform ProB Animator
http://www.event-b.org/
 
 

Tool image

B-Method
 

Atelier-B
http://www.clearsy.com/
■　Function of generating proof items automatically
■　Automatic proof
　　* Easily acquiring technologies and promoting efficiency