Main Page

Main Page

From ClearSy Tools

Jump to: navigation, search

Contents

Open Source Tools Projects

  • ComenC B to C translator The ComenC translator is a new translator for B language and allows for B0 implementations to be translated into C language.

What's new ?

Open Source Organization and strategy

If you are interested in contributing to the projects, have a look at the Open Source Organization section. Any contributor/contribution is welcome.

Our strategy is described here as well as our licensing policy.

Directions & Future Work

Integration of ProB

Image:ProB_Web2.gif
We are looking for integrating ProB model-checker in Atelier B 4.0, in order to provide additional proof power and animation capabilities to Atelier B.

With the help of Pr. Michael Leuschel, a MacOS prototype has been developped during week #3 2009, allowing to animate and model-check a B model from Atelier B 4.0. At that occasion, a generic interfacing mechanism has been developped and will be enriched and improved in the future. This mechanism is described in the GUI_Project section. ProB 1.3.0+ is now self integrating with AtelierB 4.0, at model level. Ongoing developments at University of Dusseldorf for integration at proof obligation level.

Introduction of modalities

Within the MATISSE project, a preliminary version of event-B was designed and implemented with the "eventB to B" translator. At that occasion, two modalities (establish and maintain) were specified and implemented in the translator. These modalities were used in some case-studies and proved to be interesting features to keep in the language.

We would like to revisit these modalities against modelling experience gained since then, specify and natively implement these modalities (instead of generating ASSERTIONS). A proposal is available for download and discussions.

Development of a generic proof obligation generator

Atelier B proof obligation generator was developped in the early 90's. Developped with the prolog-like "theory language", this tool is very sensible to modifications and difficult to adapt to language extensions/modifications. The idea is to develop a generic proof obligation generator that can:

  • support both B and event-B proof obligations
  • be easily modifiable/extandable

Rodin to Atelier B import wizard

Atelier B 4.0 natively supporting event B, importing Rodin models seems to be a mandatory feature to add. Rodin typechecker allowing implicit typing, a typer has to be developed, based on the B-Compiler.

Development has started in April 2009, through one internship.

Port & development of Brama model animator to Atelier B

Image:Logo_brama.jpg
Atelier B 4.0 natively supporting event B, animating such models is mandatory. The Brama animator has to be ported on Atelier B 4.0 environment: the predicateB predicate evaluator has to be ported to C++ and connected with B-Compiler.

Port has started in February 2009, through two internships.

Connection of the Predicate Prover with SMT library

Definition and implementation of XML format for information exchange

Defining an XML format for information exchange is required for enabling the connection of heterogenous tools.

Ongoing discussion and work are hosted on the XML format for information exchange page.

Tasking

Achievements

On-Going Work

Retrieved from "http://tools.clearsy.com/index.php5?title=Main_Page"