Modelling

Part 2: Modelling and Model-Based Design (C++ Context)

5. Modelling with Finite State Machines (FSM)

• Finite State Machines:

  • States, Transitions, Inputs, and Outputs.

  • Moore Machines: Output depends only on the state.

  • Mealy Machines: Output depends on state and input.

• UML State Machines:

  • Enhancements over standard FSMs.

  • Hierarchy: Composite states (nested states) to manage complexity.

  • Concurrency: Orthogonal regions for parallel behavior.

  • Pseudo-states: History states (shallow/deep), Fork/Join, Entry/Exit points.

  • Actions: Entry, Exit, and Do activities.

6. Modelling with Petri Nets

• Basic Concepts:

  • Places (circles), Transitions (bars), Tokens, and Arcs. * Firing Rules: Enabling transitions based on input tokens.

• Modelling Capabilities:

  • Sequential execution, Concurrency, Synchronization, and Conflict/Choice.

  • Mutual Exclusion modelling.

• Analysis Properties:

  • Boundedness/Safeness: Limits on token counts (memory stability).

  • Liveness: Freedom from deadlocks.

  • Reachability: Determining if specific states can be reached (Reachability Tree).

• Extensions:

  • Colored Petri Nets (Data on tokens).

  • Timed Petri Nets (Deterministic, Interval, Stochastic).

7. Verification and Model-Based Code Generation

• Formal Verification:

  • Model Checking: Exhaustive verification of system properties.

  • Computation Tree Logic (CTL):

    • Path Quantifiers: $A$ (All paths), $E$ (Exists a path).

    • Temporal Operators: $G$ (Globally), $F$ (Future), $X$ (Next), $U$ (Until).

  • Tool: NuSMV for symbolic model checking.

• Model-Based Design to Code:

  • Workflow: Model $\to$ Code Generator $\to$ Source Code (C++).

  • Tools: Rational Rhapsody (generating C++ code from UML models).

  • Advantages: Traceability, consistency between design and implementation.

  • Challenges: “Round-trip” engineering (manual code edits vs. model updates).