Verification of Scenario-based Behavioural Models using Capella and PyNuSMV

Scenarios are widely use to capture a set of key system behaviours. They are part of standardised modelling languages like UML and SysML. Precise semantics enable to analyse them at a formal level. In this paper, we show how scenarios can be used to perform early checks on behavioural models in an industrial context by providing a bridge between system modelling with Capella and the NuSMV model checker through the PyNuSMV integration library and using hMSC semantics. Both the modelling front-end and verification backend are discussed and illustrated on a case study of unmanned aerial vehicles. Some interesting extensions to increase the value of the integration are also identified and discussed.