This plugin is made to enable formal verification of SysML statechart based behavioral models in MagicDraw. To achive its goal the plugin utilizes the Gamma Statechart Composition Framework and UPPAAL by introducint a tranformation to Gamma's Statechart language which can be translated to UPPAAL models.
- Transform statecharts to Gamma's statechart language
- Tranform composite models to Gamma's composite language
- Perform the formal verification using Gamma and UPPAAAL
- Introduce a new way to define the verifiable properties
- Generate simulations of erroneous behaviors