From ClearSy Tools
Hilights & Forthcoming
|
- Developing software with the B method
- The C4B code generator explained
- Proof Obligation Demonstration Strategy
- The Small Automatic Train Protection Software example
- Requirements Traceability
- Bart B automatic refinement tool This tool allows for a B0 implementation for a machine or a sufficiently detailed B refinement to be automatically generated.
- B to C translator The C4B translator is a new translator for B language and allows for B0 implementations to be translated into C language.
|
|
What's new ?
|
|
Due to regular intensive spam on this wiki, access is now restricted while security is improved through group-based rights. More than 1800 pages and user accounts have been deleted. If you want to contribute or if your account has been deleted by mistake, just contact us at open-source at clearsy.com.
|
|
Directions & Future Work
Integration of ProB
|
|
| ProB model-checker is being integrated 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, 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.
|
|
|
|
| Atelier B 4.0 natively supporting event B, animating such models is mandatory. The Brama animator has been ported on Atelier B 4.0 environment: the predicateB predicate evaluator has been ported to C++ and connected with B-Compiler.
|
|
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
Developments started in 2011, within the framework of the CERCLES-2 R&D project.
|
|
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.
|
|
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
- Atelier B 4.0 GUI being translated in Japanese
- Requirements Management plugin under development
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.
