形式手法Bメソッド研修セミナー | 先端ソフトウエア工学に関するGRACE国際シンポジウム 2010

オーガナイザ	Thierry Lecomte (ClearSy)
概要	The aim of this workshop is to illustrate B/event-B formal modeling as a technique for specifying, designing, coding and validating software-based systems. Backed with the two main open-source modeling platforms (RODIN, Atelier B) and in relation with the growing number of industrial applications in the Railways and in the Smartcard domains, this workshop is headed at providing a clear picture of B/Event-B current status of development and exploitation, focusing on the support tools as well as the industrial applications. The workshop includes a large scope of presentations given by the DEPLOY project members or associated to the project results. Target audience is software/system engineers and project managers, as well as researchers in the domain.

オーガナイザ

Thierry Lecomte (ClearSy)

概要

The aim of this workshop is to illustrate B/event-B formal modeling as a technique for specifying, designing, coding and validating software-based systems.

Backed with the two main open-source modeling platforms (RODIN, Atelier B) and in relation with the growing number of industrial applications in the Railways and in the Smartcard domains, this workshop is headed at providing a clear picture of B/Event-B current status of development and exploitation, focusing on the support tools as well as the industrial applications. The workshop includes a large scope of presentations given by the DEPLOY project members or associated to the project results.

Target audience is software/system engineers and project managers, as well as researchers in the domain.

Session1	The Big Picture: 15 min. (T. Lecomte)
	System-level modeling with Event B: 45 min. (M. Butler)
	The Rodin platform: 30 min. (M. Butler)
Session2	Model checking and animation with ProB: 30 min. (M. Leuschel)
	UML-B: 20 min. (M. Butler)
	Code generation : 40 min. (T. Lecomte / A. Requet) Sequential code in C / Ada PLCs VHDL
Session3	Automatic refinement: 15 min. (A. Requet)
Session3	Industrial applications: 1 hour 15 min. Automatic pilots (Siemens, Alstom): (T. Lecomte) Validation of large scale railway models: (M. Leuschel) Event-B in space (Space System Finland case study) Formal Development of Enterprise Service Communication (SAP case-study) Smartcard (Memory Protection Unit from STMicroelectronics): (T. Lecomte)