DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B
In conjunction with
ICFEM 2012
Nov 13, 2012
Kyoto, Japan
Important Dates
Submission Deadline:
Aug 19, 2012
(extended)
Notification:
Sep 10, 2012
Camera-ready Copy Due
Oct 10, 2012
Workshop:
Nov 13, 2012
Contact:
f-ishikawa<-at->nii.ac.jp
Links
ICFEM 2012
CbC-Depend Tutorial
Sponsers
Proceedings
Available as a technical report at Newcastle University and on ACM CoRR.
Program
See the links below for details of the invited talks.
- Business Application Development -Ensuring Dependability through Formal Methods, Andreas Roth (SAP, Germany)
- DSF Activities: Applying Event-B to Business Application Software (Dependable Software Forum, Japan)
Final Program updated on Oct 19.
8.45-9.00 Welcome
9.00-10.00 Invited Talk (1)
Andreas Roth (SAP, Germany): Business Application Development - Ensuring Dependability through Formal Methods
10.00-10.25 Technical Talks
Andreas Fürst, Thai Son Hoang, David Basin, Kunihiko Miyazaki and Naoto Sato: Abstract Data Types in Event-B – An Application of Generic Instantiation
10.25-10.40 Brief Announcements
Systerel and ADVANCE
10.40-11.00 Coffee Break
11.00-12.40 Technical Talks
Inna Pereverzeva, Elena Troubitsyna and Linas Laibinis: Development of Fault Tolerant MAS with Cooperative Error Recovery by Refinement in Event-B
Andrew Edmunds, Michael Butler and John Colley: Building on the DEPLOY Legacy: Code Generation and Simulation
Renato Alexandre Silva: Lessons Learned/Sharing the Experience of Developing a Metro System Case Study
Alexei Iliasov: Event-B/SLP
12.40-12.55 Brief Announcements
ClearSy and Rodin Tools
12.55-14.00 Lunch
14.00-14.45 Invited Talk (2)
Yuusuke Hashimoto (NEC and Dependable Software Forum, Japan): DSF Activities: Applying Event-B to Business Application Software
14.45-15.35 Technical Talks
Thai Son Hoang: Proof Hints for Event-B
Tsutomu Kobayashi and Shinichi Honiden: Towards Refinement Strategy Planning for Event-B
15.35-16.00 Coffee Break
16.00-17.40 Technical Talks
Thierry Lecomte, Lilian Burdy and Michael Leuschel: Formally Checking Large Data Sets in the Railways
Alexei Iliasov and Jeremy W. Bryans: A recipe for timed Event-B specifications
Elena Troubitsyna: Dependability-explicit engineering with Event-B: overview of recent achievements
Frédéric Badeau and Marielle Doche-Petit: Formal Data Validation with Event-B
17.40-17.50 Close
Invited Talk 1: Business Application Development -Ensuring Dependability through Formal Methods
Andreas Roth (SAP, Germany)
Business applications integrate data and services of various organizational units across an entire company and therefore form large and complex systems. Their business criticality imposes severe requirements concerning their dependability while their development cycles need to be fast and efficient. In this talk we report on the experience we collected about the lightweight use of Formal Methods (and in particular Event-B) in the development of business applications during the DEPLOY project. We will present our deployment approach exemplified on the service integration and business process layer. Furthermore we will point to challenges to be solved regarding recent trends in business applications.
Invited Talk 2: DSF Activities: Applying Event-B to Business Application Software
Yuusuke Hashimoto (NEC, Japan), Hironobu Kuruma (HITACHI, Japan), and Shin Nakajima (NII, Japan)
In Japan, the quality of software becomes a social issue and the software industry is more interested in formal methods than before. Formal methods, however, are not broadly used in the area of business applications. To promote formal methods including Event-B in this area, six major IT companies (NTT DATA, FUJITSU, NEC, HITACHI, TOSHIBA and SCSK) and NII formed a joint research group, DSF (Dependable Software Forum). After some studies DSF released a set of documents “Guidelines to use Formal Methods”. Then DSF joined a working group of IPA (Information-technology Promotion Agency, Japan) to conduct a feasibility study of formal methods including Event-B. Using these formal methods, we could successfully recapture bugs in design documents. They had been found in the later phases in the original development. DSF was dismissed in June 2012 and its participant companies are now promoting the use of formal methods in their software development.