Compatibility Verification of SysML Blocks Using Hierarchical Interface Automata

The objective of this paper is to propose an approach to formalize and verify the compatibility between SysML blocks, and to help in making decision about the possibility of assembling these blocks. We specify the architecture of the system using SysML internal block diagrams. To model the interaction between blocks with a convivial manner, we propose HPSM (Hierarchical Protocol State Machine) diagram. In order to permit the verification of such interactions, we perform a translation of HPSMs into HIA-ILTs (Hierarchical Interface Automata with Inter-Level Transitions), a variant of interface automata (IA) which we propose for this purpose. Our major objective is to benefit from the hierarchy which is present in HIA-ILTs. Thus, we have adapted the existing approaches of compatibility verification based on IAs to be applicable on the HIA-ILTs. However, in order to avoid the flattening of the entire HIA-ILT, we propose a preliminary phase that allows selecting the composite states to flatten. The aim behind this is to alleviate the verification phase. Our approach is illustrated by a case study, where we demonstrate the expressiveness of the HPSM and the HIA-ILT, and we show how the hierarchy and the abstraction help to reduce the complexity of verification.