Upgrade to Pro — share decks privately, control downloads, hide ads and more …

V&V of Systems Engineering Models and Modeling Languages

Critical Systems Research Group
October 10, 2023
Research
0
97

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.

Critical Systems Research Group

October 10, 2023
Tweet

More Decks by Critical Systems Research Group

See All by Critical Systems Research Group
Lazy Abstraction for Markov Decision Processes
ftsrg
0
10
Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
ftsrg
0
12
The many meanings of UML 2 Sequence Diagrams: a survey
ftsrg
0
100
Automated isolation for white-box test generation
ftsrg
0
45
Classifying generated white-box tests: an exploratory study
ftsrg
0
130
Gazer-Theta: LLVM-based Verifier Portfolio with BMC-CEGAR
ftsrg
0
28
Evaluating and Improving White-Box Test Generation
ftsrg
0
11
Effective Domain-Specific Formal Verification Techniques
ftsrg
0
14
SMT-Friendly Formalization of the Solidity Memory Model
ftsrg
0
10

Other Decks in Research

See All in Research
Synthetic Control Methods through Predictive Synthesis
masakat0
0
110
Unisim 超リアルな自動運転センサシミュレーション
abemii
1
670
Instituto Sumaúma | Apresentação Institucional 2023
sumauma
1
170
PiCoP en
hiroyaonoe
0
210
CVPR 2023 速報：CCC Summer 2023 in MIRUチュートリアル（配布版）
gatheluck
4
2.9k
RSJ2023「基盤モデルの実ロボット応用」チュートリアル2（実ロボット用の基盤モデルを作って活用する方法）
tmats
1
600
SNLP2023: Can Large Language Models Be an Alternative to Human Evaluations?
shotasasaki
0
290
Mean-Variance RL (JAFEE 2023)
masakat0
1
280
Off-Policy Evaluation of Ranking Policies under Diverse User Behavior (日本語版)
aiueola
0
180
FINN (Fire INventory from NCAR)のための地理情報処理：山火事からの大気汚染物質排出量の推計
yosukefk
0
200
New algorithms for collaborative text editing
ept
0
120
エッジコンピューティングとelixir
kikuzo
3
190

Featured

See All Featured
KATA
mclloyd
13
11k
Web development in the modern age
philhawksworth
200
9.9k
Ruby is Unlike a Banana
tanoku
93
9.9k
The Cult of Friendly URLs
andyhume
71
5.4k
Art Directing for the Web. Five minutes with CSS Template Areas
malarkey
197
11k
Intergalactic Javascript Robots from Outer Space
tanoku
264
26k
jQuery: Nuts, Bolts and Bling
dougneiner
57
6.8k
Atom: Resistance is Futile
akmur
257
24k
JavaScript: Past, Present, and Future - NDC Porto 2020
reverentgeek
39
3.9k
Robots, Beer and Maslow
schacon
154
7.6k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
33
8.6k
Build The Right Thing And Hit Your Dates
maggiecrowley
23
1.7k

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

    View Slide

  2. 4th WAFERS @ ISSRE 2023
    Critical cyber-physical systems
    Complex. Safe. Secure.

    View Slide

  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

    View Slide

  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

    View Slide

  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

    View Slide

  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

    View Slide

  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

    View Slide

  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?

    View Slide

  9. Can we use formal verification
    “as a service” on industrial-scale
    executable SysML models?

    View Slide

  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

    View Slide

  11. 4th WAFERS @ ISSRE 2023
    Selected elements and environment
    Selected tools and environment

    View Slide

  12. 4th WAFERS @ ISSRE 2023
    • Containerized deployment
    • Model checker runtime service
    • UI: Jupyter notebook
    V&V workflow

    View Slide

  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

    View Slide

  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

    View Slide

  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

    View Slide

  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?
    😕
    😐
    🙂
    😐
    🎉
    😕
    😕
    ⚠️

    View Slide

  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…
    … /…
    … /…
    🗸 – – –
    🗸 – – –
    🗸 – – –
    +

    View Slide

  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
    🗸
    🗸
    ✗
    ▶

    View Slide

  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…
    … /…
    … /…
    🗸 – – –
    🗸 – – –
    🗸 – – –
    +

    View Slide

  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

    View Slide

  21. 4th WAFERS @ ISSRE 2023
    Abstraction level of execution traces

    View Slide

  22. 4th WAFERS @ ISSRE 2023
    Semantics is especially hard with doActivities
    Identified
    patterns

    View Slide

  23. 4th WAFERS @ ISSRE 2023
    V&V of Systems Engineering
    Models and Modeling Languages

    View Slide