Tuesday, June 15, 2010

Workshop on B Dissemination

Workshop on B Dissemination

November 8-9, 2010
Natal, Brazil

Satellite event of SBMF 2010 <


This B / event-B workshop is organized on behalf of the 
DEPLOY project 
Its objectives are to present current 
status and ongoing research
and development related to B and 
event B languages and tools, as well as 
applications to industry size problems.
Topics addressed by the workshop are many,
including but not limited to:

* Tool development (language extensions,
external provers, code
generation, etc.)
* Modelling challenges (real time properties, probabilistic
refinement, design patterns, high order logic, etc.)
* Deployment (methodology, cases-studies, return of experience,
scaling up, etc.)
* Teaching and training

Researchers are invited to contribute to the
second day of the workshop 
through an open call for papers.


The workshop lasts 2 days:

* The first day is devoted to DEPLOY speakers. 
General presentation
of the project and tools will be sided by 
focused talks on
matters (modelling time, code generation, 
model animation, model
checking, etc.) that are being researched in DEPLOY.
Reports on industrial applications (space, 
railways, automotive,
information systems, etc.) will complete the day.
* The second day is open to any presenter, 
through an international
 call for papers. Expected contributions would 
range from theoretical research to
practical applications of B/event B. 
Submissions are handled by
the programme committee.

The workshop is collocated with the SBMF
conference (Monday and 
Tuesday), at the Imira Plaza hotel &lt

Important Dates
* Paper submission deadline: 30 July 2010
* Notification of acceptance/rejection: 
06 September 2010
* Workshop in Natal, Brazil: 08-09 November 2010

Submission and attendance

We anticipate a rich exchange of ideas and discussions 
during this event. Submissions are welcomed on any
subject that falls within the main issues.
Papers should be around 6 pages in ENTCS style.

All papers must be submitted in PDF format, 
following the instructions at the WOBD'10 submission 
site, handled by EasyChair:

All accepted papers should be presented during the workshop.

 Workshop Chair:
* Thierry Lecomte <
mailto:thierry.lecomte@clearsy.com> (ClearSy)

 Program Committee:

* Michael Butler (University of Southampton, UK)
* Clif Jones (University of Newcastle, UK)
* Jérôme Phalampin (Siemens Transportation Systems, France)
* Lilian Burdy (ClearSy, France)
* David Basin (ETH Zurich, Switzerland)
* Michael Leuschel (University of Dusseldorf, Germany)
* Mathieu Clabaut (Systérel, France)
* Christophe Ponsard (CTIC, Belgium)
* Elena Troubitsyna (University of Turku, Finland)
* Rainer Gmehlich (Bosch, Germany)
* Aryldo Russo (AeS, Brazil)

Tuesday, June 8, 2010

B方法 , The B Book in chinese



General-Service Ballistic Computer Programming Based on B-Method

"Formal methods offer the promise of significant improvement on quality and reliability of critical embedded software. B-Method is employed to develop general-service ballistic computer programs in the paper, each of which can be adapted to a family of service/weapon-specific ballistic computers. Based on the structuring mechanisms of B-method, a unified approach is proposed to systematically control the complexity of ballistic parameters in the process of type and operation refinement, and ultimately a series of high reliable, reusable, and scalable programs are produced. Experiences with the application of the method and tools are also discussed."

Formal development of a washing machine controller by using formal design patterns


Event Model Decomposition


The papers and the slides of the conference 2010 are here ...