MODELS2021 success with over 460 attendees
MODELS 2021: ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems was successfully held last week (October.10-15) virtually with over 460 attendees from all over the world. We, ChangeVision, Inc. participated as a sponsor and a few members from Change Vision, Inc. attended as a host and a speaker.
The MODELS conference always have this traditional program called “the Industry Days” that is where leading engineers, researchers, and managers of key industrial players in various application domains give a technical presentation to summarize future trends and ongoing innovative projects.
“Lightweight integration of MBSE and model-checking”
Toshinori Takai from Change Vision, Inc. gave a presentation about “Lightweight integration of MBSE and model-checking” during the industry days. In his presentation, he shared the background of MBSE and latent difficulties of applications of model-checking techniques and how well these two would meet and the positive result the collaboration of model-checking and MBSE will engender that we expect to see.
He showed some case studies of adopting the model-checking approach in the MBSE for road vehicle subsystems and described the key roles of model-checking in MBSE.
He summarized the studies and shared the following four future directions that the collaboration of model-checking/simulation for MBSE should drive to:
- Use SysML models to describe verification properties
- Automatically elicit verification properties from SysML models
- Integrate model-checking techniques with risk/hazard analysis activities
- Use the results of model-checking tools for safety argumentation
After the presentation, he received several questions below and had a productive discussion with the audiences. (If you’re interested in the answers to these questions, please leave your comment!)
- Is there any publication on the translation from SysML to Promela (the modeling language for Spin model-checker)?
- How can we input verification properties of model-checking for that tool?
- Who do you assume will be doing the work in a real project ?
- How do you avoid the “state explosion problem”?
Full presentation slide is available if you’re interested.
A MBSE tool used in the presentation
SysML diagrams used in the preseation are created by Astah System Safety. This product does not only support MBSE but also covers the mentioned four future trends: risk/hazard analysis activities using STAMP/STPA and safety argumentation using GSN (Goal Structuring Notation).
If you’re interested, you can try out this product for 40 days for free.
Astah in 5min 
One thought on ““Lightweight integration of MBSE and model-checking” Oct. 13, 2021@Industry Day, MODELS2021”