Formalizing and verifying compatibility and consistency of SysML blocks

The objective of this paper is to define an approach to formalize and verify the SysML blocks in a refinement process. We propose to specify system architecture with SysML Block Definition Diagram, this diagram is then analyzed and decomposed into several sub-blocks in order to verify 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. The behaviour of each sub-block is described by an interface automaton which species 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 deadlocks during the interaction between sub-blocks. Once the verification is established between the sub-blocks, the abstract block can be then substituted by the sub-blocks which compose it.