V&V of Systems Engineering Models and Modeling Languages

Model-based development is an often-used technique in the context of cyber-physical systems. Systems engineering modeling languages, like SysML, offer many benefits, including early verification and validation of key system behavior. However, in safety-critical systems requiring strong guarantees, V&V needs to be holistically applied to both the models and the modeling tools at multiple meta-levels. This talk will present results on the V&V of the engineering models and the modeling languages used to create those models stemming from multiple international collaborations.

Transcript

1. V&V of Systems Engineering Models and Modeling Languages 4th WAFERS @ ISSRE 2023 micskeiz mit.bme.hu/~micskeiz Zoltán Micskei Budapest University of Technology and Economics
2. 4th WAFERS @ ISSRE 2023 Critical cyber-physical systems Complex. Safe. Secure.
3. 4th WAFERS @ ISSRE 2023 Modeling in Systems Engineering Systems Engineer Software Engineer Requirements Systems Engineer System design Simulation, test scenarios Source of figures: R. Karban et al. ESEM: Automated Systems Analysis using Executable SysML Modeling Patterns. DOI Software design Code Platform
4. 4th WAFERS @ ISSRE 2023 • Design modeled with SysML • Available from OpenMBEE Example: Thirty Meter Telescope (TMT) S. Herzig et al. Analyzing the Operational Behavior of the Alignment and Phasing System of the Thirty Meter Telescope using SysML. DOI
5. 4th WAFERS @ ISSRE 2023 Executable behavior: • state machines + • detailed activities Example: Thirty Meter Telescope (TMT) S. Herzig et al. Analyzing the Operational Behavior of the Alignment and Phasing System of the Thirty Meter Telescope using SysML. DOI
6. 4th WAFERS @ ISSRE 2023 Modeling in Systems Engineering Systems Engineer Software Engineer Requirements Systems Engineer System design Simulation, test scenarios Source of figures: R. Karban et al. ESEM: Automated Systems Analysis using Executable SysML Modeling Patterns. DOI Software design Code Platform V&V of models V&V of modeling languages & tools
7. V&V of SysML Models Model Checking as a Service 4th WAFERS @ ISSRE 2023 B. Horváth, V. Molnár, B. Graics, Á. Hajdu, I. Ráth, Á. Horváth, R. Karban, G. Trancho, Z. Micskei Pragmatic verification and validation of industrial executable SysML models. Syst. Eng. 2023; 1-22. DOI
8. 4th WAFERS @ ISSRE 2023 Modeling in Systems Engineering Systems Engineer Software Engineer Requirements Systems Engineer System design Simulation, test scenarios Source of figures: R. Karban et al. ESEM: Automated Systems Analysis using Executable SysML Modeling Patterns. DOI Software design Code Platform V&V of models What if review, simulation & model-level testing is not enough?
9. Can we use formal verification “as a service” on industrial-scale executable SysML models?
10. 4th WAFERS @ ISSRE 2023 • Several constructs result in demanding verification problems – E.g., non-determinism in orthogonal region and doActivity • Large and complex models – E.g., TMT PEAS function: 10 states, 739 actions… • Tools and engineers might interpret constructs differently Challenges of verifying executable SysML Select a pragmatic subset where formal verification could be feasible
11. 4th WAFERS @ ISSRE 2023 Selected elements and environment Selected tools and environment
12. 4th WAFERS @ ISSRE 2023 • Containerized deployment • Model checker runtime service • UI: Jupyter notebook V&V workflow
13. 4th WAFERS @ ISSRE 2023 • Supporting some executable action, guard language, and activity diagrams is a must to verify industrial models. • Finding a pragmatic subset of the modeling language can help to reduce the ambiguity in interpretation. • Support the policies and requirements of the corresponding enterprise (authentication, multiple users, logging..). • Sometimes restricting the explored state space has to be chosen to scale to industrial models. Lessons learnt
14. V&V of modeling languages with M. Elekes, V. Molnár 4th WAFERS @ ISSRE 2023 Elekes, M., Molnár, V. & Micskei, Z. Assessing the specification of modelling language semantics: a study on UML PSSM. Software Qual J 31, 575–617 (2023). DOI Elekes, M., Molnár, V. & Micskei, Z. To Do or Not to Do: Semantics and Patterns for Do Activities in UML PSSM State Machines. Preprint, arXiv:2309.14884 (2023). DOI
15. 4th WAFERS @ ISSRE 2023 Modeling in Systems Engineering Systems Engineer Software Engineer Requirements Systems Engineer System design Simulation, test scenarios Source of figures: R. Karban et al. ESEM: Automated Systems Analysis using Executable SysML Modeling Patterns. DOI Software design Code Platform V&V of modeling languages & tools
16. 4th WAFERS @ ISSRE 2023 Subset of traces users and tools explore ALL possible traces of the model Traces envisioned by MODEL USERs Misunderstanding semantics? How well- defined is the semantics? Traces that could be produced by SIMULATORs Simulator not conforming to specification Traces that could be produced by model VERIFIERs Explored state space is usually smaller Is the mapping to formal models correct? Insufficient features? 😕 😐 🙂 😐 🎉 😕 😕 ⚠️
17. 4th WAFERS @ ISSRE 2023 Language artefacts and how to check them formalise Specification rule { ⋮ } informal text semi-formal semantics Impl. void f() { return; } refine Verifier SMT 𝒄 𝟏 𝟏 ,… , 𝒄𝒏 𝒏 ሥ 𝑜𝑝 i i ⊨ infer execute defines compare implement test design Artefacts Understanding verify ⑨ Test suite S… S… S… S_ S… … /… … /… 🗸 – – – 🗸 – – – 🗸 – – – 🗸 – – – + illustrate S… S… S… S_ S… … /… … /… 🗸 – – – 🗸 – – – 🗸 – – – +
18. 4th WAFERS @ ISSRE 2023 • UML – General-purpose modelling language for software systems – Several diagram types for different aspects • OMG defined PSSM (Precise Semantics of UML State Machines) – Based on fUML – Execution semantics – Test suite – Check tool conformance with the specification – Illustrate the semantics • + reference implementation Case study: Precise Semantics of State Machines 🗸 🗸 ✗ ▶
19. 4th WAFERS @ ISSRE 2023 Artefacts to PSSM and their understandings formalise Specification rule { ⋮ } UML informal text PSSM semi-formal semantics Impl. Cameo, Moka void f() { return; } refine Verifier SMT 𝒄 𝟏 𝟏 ,… , 𝒄𝒏 𝒏 ሥ 𝑜𝑝 i i ⊨ infer execute compare implement test design Artefacts Understanding ⑨ Test suite PSSM S… S… S… S_ S… … /… … /… 🗸 – – – 🗸 – – – 🗸 – – – 🗸 – – – + illustrate S… S… S… S_ S… … /… … /… 🗸 – – – 🗸 – – – 🗸 – – – +
20. 4th WAFERS @ ISSRE 2023 Explicitly represent semantic concepts in the spec. & traces Abstraction level of execution traces (what is observable?) Generate the expected execution trace Difficulty: a simulator generates a single trace or non-deterministically Separate tests for tools and readers Tooling and semantics in early development stages Recommendations for new languages
21. 4th WAFERS @ ISSRE 2023 Abstraction level of execution traces
22. 4th WAFERS @ ISSRE 2023 Semantics is especially hard with doActivities Identified patterns
23. 4th WAFERS @ ISSRE 2023 V&V of Systems Engineering Models and Modeling Languages