BRILLANT: an open source and XML-based platform for rigourous software development

摘要

The need for the B method first appeared in industry, and several commercial tools have been developed to support this formalism. However, few of these tools allow reasoning on the formalism itself or on its possible extensions. This article presents an open-source platform, with a focus on the platform's core component, the BCaml project. The tools presented are used to show how very different approaches can be brought together around a central design to form a consistent toolbox, and can be used to develop safe systems, from their specifications to their validation and the generation of safe code.