Formal modeling with SysML

Often designated as a UML profile for system modeling, SysML brings some changes that enhance the possibilities of describing systems specificities, but raise new criticisms on the language interpretation. In the last SysML standard document, the new concepts are presented in an informal manner and the revised ones are often described in a way that makes difficult the appreciation of the changes. The internal block diagram, which replaces the UML composite structure diagram, is of interest regarding the innovative concepts it introduces in the old notation. We propose, in this paper, to formalize the semantics related to both of its structure and behavior. To conduct the formalization in an efficient manner, we go towards a semantic domain that fits the diagram characteristics. Hierarchical Colored Petri Nets constitute an appropriate choice. The formalization is validated by model checking. A case study, based on a system that meets the specific features SysML has been intended to model, illustrates the approach throughout the paper.