SysML to B translator - V&V for Systems Engineering

Document Actions

Proprietary tool based on an alignment of SysML with the B Method. Author: Erwan Bousse

Introduction

This page presents a proprietary prototype written during my internship at MERCE (Mitubishi Electric Research Center Europe). It consists in transforming SysML models into B method models.

Master thesis work : abstract

The use of formal methods in an industrial context is still uncommon, even among safety critical systems design processes. Yet, formal approaches like the B-method have proven successful on large-scale projects. On the other hand, certification authorities and system designers rely more and more on semi-formal languages such as UML or SysML. The objective of our work is to identify a way to jointly use existing semi-formal languages for design and formal methods for verification of safety properties. Our approach is based on a deep analysis of both languages semantics, and on the definition on a model-to-model transformation. We apply this method and design a process that translates SysML models into B projects at the implementation level. This process is successfully executed on a simplified railway system specification. With these positive results, we conclude that such a global approach may open interesting perspectives.

Link to the whole master thesis: http://people.irisa.fr/Benoit.Combemale/research/2012/bousse_erwan_report.pdf

Prototype

To provide a proof-of-concept tool with our SysML→B-method translation rules, we implemented a model-to-model transformation using Kermeta, a metaprogramming environment and a language optimized for metamodel engineering.

This figure shows the complete Model Driven Engineering (MDE) process we put in place. The first step is a model-to-model transformation developed in Kermeta that takes an SysML model encoded using the XML Metadata Interchange (XMI) standard, and transforms it into a B-method model kept in memory for the next step. Such SysML models can be drawn using any modeling tool that can export to this format while using the official SysML metamodel – defined in multiple .ecore files by the Object Management Group (OMG). The B model obtained is an instance of the B metamodel we defined ourselves, and is the input of a text-to-model transformation also written in Kermeta. This second step generates a B concrete project using the Atelier B syntax. Then, the files can directly be imported into Atelier-B in order to generate proof obligations, and to use the theorem prover included.

Algorithm sample: creating and linking B modules from SysML blocks

Since the prototype is the property of Mitsubishi Electric, we cannot show the code nor code samples. However, here is an example of how the translation works for SysML blocks into B modules.

In our work environment, we have SysML metamodel imported as well as B metamodel. We use aspect-oriented programming to decorate SysML metaclasses that must be transformed, adding:

a reference to the object we want to obtain with the translation
a first pass operation 'build' that constructs this object
a second pass operation 'link' that links this object to all the others (called after all other 'build' operations)

We do this for each SysML metaclass whose instances must be transformed in B metamodel instances. The starting point relies in the root package of the SysML model: blocks inside this package are found, and their build operations are called (which will in turn call the build operations of the objects they contain or refer). Then, all the link operations of the blocks are called (which will in turn call the link operations of the objects they contain or refer). Finally, we gather all the b::Machine instances created as bMachine references in blocks, and obtain a complete B project.

aspect class Block
{
    /**
     * The machine in which the class is transformed.
     */
    reference bMachine : b::Machine

    ...

    /**
     * Constructs the 'bMachine' attribute.
     */
    operation build(): Void is do
        // We consider that each block becomes a B module, which means an abstract machine and an implementation
        self.bMachine := b::BMachine.new
        self.bMachine.name := self.name
        self.bMachine.refinedBy := b::Implementation.new
        self.bMachine.refinedBy.name := self.bMachine.name+"_i"
        self.bMachine.refinedBy.refines := bMachine
        // For each attribute of the block (references, values, etc.)
        self.ownedAttribute.each{prop|
            // We call the build operation of the attribute
            prop.build()
            // And we find out what was build (many possibilities)
            if prop.bVariable != void then
                self.bMachine.abstractVariables.add(prop.bVariable)
            end
            if prop.bConcreteVariable != void then
                self.bMachine.refinedBy.concreteVariables.add(prop.bConcreteVariable)
            end
            ...
        }
        ...
    end

    /**
     * Links the 'bMachine' instance to other elements of the B model.
     */
    operation link(): Void is do
        ...
        // We call the link operation of the attributes
        self.ownedAttribute.each{prop|prop.link()}
        ...
    end

}