Mark Bouwman: Direct formalization of EULYNX SysML in mCRL2


Event Details


FormaSig aims to strengthen railway signalling standardization processes with the use of formal methods. The concrete approach investigated in FormaSig is to derive formal mCRL2 models from existing SysML specifications. These formal models are then used for two distinct purposes: (i) checking whether the original standard satisfies the requirements that are imposed upon them, and (ii) performing automated testing of implementations. In this talk I will present our approach to developing a translation from SysML to mCRL2. We define the semantics of state machines directly in mCRL2. The model containing the generic semantics then only needs to be completed with a specific instantiation of state machines by encoding the structure of these state machines in the mCRL2 data language. We have a prototype translation tool that takes a number of SysML diagrams and produces such a configuration.