面向高信赖软件开发，采用了形式化方法(FormalMethod)的开发过程的研究
在国内外，IT担负着重要的社会基础，一些软件错误正逐渐成为重大的社会问题。
现在电子装置开发•嵌入式软件开发的规模日益增大且复杂化，因此软件的品质保持变得非常困难。
面对上述的现况,构筑高信赖软件开发,进行研究着形式化方法(B-Method,Event-B)的开发过程。

※对于日本经济产业省中小企业厅公开招募的《2010年度战略的基础技术高度化支援事业》,采纳了《用形式化规格记述高信赖软件开发进程的研究与工具开发》,已受到3年的实业委托

形式化方法是什么？
设计•检验的方法之一:基于数理逻辑学,表示以有严密语义的语言说明要求。
1.形式化规格描述
记述规格用基于数学•逻辑学的严密《规格记述语言》。
2.形式化的检验
用支援道具,发现《规格记述语言》记述的规格中的不一致性和疵点。