Formalizing and Verifying Compatibility and Consistency of SysML Blocks

International audienceThe objective of this paper is to define an approach to formalize and verify the SysML blocks in a refinement process. From a Block Definition Diagram which specifies system architecture, it is a matter of decomposing it into several sub-blocks, then of verifying their compatibility. The structural architecture of an abstract block is given by the Internal Block Diagram (IBD) which defines the communication links between sub-blocks. The compatibility verification between sub-blocks is only made on linked sub-blocks. Thebehaviour of each sub-block is described by an interface automaton which specifies the invocations exchanged with its environment. The verification between blocks is translated into consistency verification between the blocks and compatibility verification between their interface automata. Incompatibilities can be inconsistent at architecture level and at communication level if there are illegal states. Once the verification is established between the sub-blocks, the abstract block can be then substituted by the sub-blocks which compose it