Rodin plugin to link Event-B and SPIN (ソフトウェアサイエンス)

スポンサーリンク

概要

• 論文の詳細を見る

• Rodin is an eclipse-based platform dedicated to the Event-B formal modeling of systems including concurrent ones. It provides mathematical proof assistance for formal verification of the properties of systems. Basically, only safety aspects of systems are dealt with using this approach. We explain how behavioral analysis of Event-B could be applied, and describe it on a particular example. Then, we introduce our extension in a way of a plug-in for the Rodin platform that allows behavioral analysis of the Event-B descriptions using the SPIN model-checker.

• 社団法人電子情報通信学会の論文
• 2009-07-30

著者

• NAKAJIMA Shin

  National Institute of Informatics

• Muller Thomas

  National Institute Of Informatics

• Nakajima Shin

  National Inst. Informatics Tokyo Jpn

関連論文

• Highly Reliable Embedded Software Development Using Advanced Software Technologies(Software Engineering for Embedded Systems)
• Rodin plugin to link Event-B and SPIN (ソフトウェアサイエンス)
• Verification of BPEL Workflows Design using Model Checking

スポンサーリンク