## Video

Not enough ratings.

## Terminology, Model Types and Model Semantics

1
30
31
128
221
354
539
779
849
876
982
1333
1364
1493
1533
1612
1991
2257
2369
2370
2595
2929
2973
3040
3148
3179
3198
3212
3235
3320
3347
3423
3432
3477
3600
3648
3703
3829
4207
4275
4337
4339
4361
4541
4632
4712
4823
4966
4999
5062
5201
5238
5307
5345

Lecture Structure

- Outline (00:00:30)
- and Outlook (00:00:30)
- VII Verification Validation (00:00:30)
- IV Requirements (00:00:30)
- III Application Domains Life Cycle (00:00:30)
- II Foundations (00:00:31)
- Terminology (00:02:08)
- Specification A formal description of a system or a component of a system intended as a basis for further development of the specification may be in text in a natural language English in a specification which may be a language and by the use 0 specification stages of that includes a diagrammatic technique I I i e F B p than el H I (00:02:08)
- certain properties of the referent In computing models are and are typically represented in a notation such as diagrams in functional R a model or state transition diagrams for a model (00:02:08)
- Models vs Specifications (00:03:41)
- Different Kind of Models (00:05:54)
- Formal Relations Between Models (00:08:59)
- Specification specification (00:08:59)
- n Approximation M approx M M is an approximation of M (00:08:59)
- n Refinement M Q M M is a refinement (00:08:59)
- Models Preservation of Properties (00:14:08)
- Often structural similarities with (00:14:08)
- Realize the more detailed (00:14:08)
- The models become more detailed (00:14:08)
- Stepwise Refinement (00:14:09)
- Refinement vs Approximation (00:16:22)
- details will likely be found (00:16:22)
- n approach a solution for the (00:16:22)
- approach (00:16:22)
- II Foundations (00:22:13)
- Types (00:22:44)
- Considered Model Types (00:24:53)
- State M chine (00:25:33)
- Timed (00:26:52)
- Continuous Behavior (00:33:11)
- Falling Ball Example (00:37:37)
- equation (00:39:29)
- continuous I (00:39:29)
- guard (00:39:29)
- continuous variable z with (00:39:29)
- Clock (00:39:29)
- Hybrid (00:39:30)
- equation L (00:39:30)
- continuous variable z with (00:39:30)
- Clock (00:39:30)
- Continuous equations per state (00:39:30)
- Basic extension to timed (00:39:30)
- Bouncing Ball Examples (00:43:15)
- Variable Structure (00:48:49)
- Revisited (00:49:33)
- Petri Nets (00:50:40)
- Limitation still no change of S possible (00:50:40)
- The state space is a over S (00:50:40)
- T a set of transitions (00:50:40)
- S a set of places (00:50:40)
- State space s ES (00:50:40)
- Graph Transformation Systems (00:52:28)
- Example (00:53:00)
- Extended Example (00:55:47)
- I Map behavior (00:55:47)
- Track (00:55:47)
- Track (00:55:47)
- I Behavior (00:55:47)
- I Map structure (00:55:47)
- II Foundations (00:57:03)
- II 3 Model Semantics (00:57:12)
- h i LC 4 Operational Semantics describes how a valid program as sequences of computational steps These are the meaning of the program Often represented as a system (00:57:12)
- Semantics describes the meaning of a what the denotes some kin d 0 mathematical object of are partial functions X (00:57:12)
- n construct the state (00:57:57)
- Mathematical Prerequisites (01:00:00)
- Considered Model Types (01:00:48)
- State (01:01:43)
- Formal Semantics (01:03:49)
- Where all J I u 1 1 1 slate modifications (01:03:49)
- the resulting state if a x which C (01:03:49)
- z is enabled in state x l Q (01:03:49)
- max e me id gad 9 E D V u e Jar g e (01:03:49)
- finite set of T a finite set transitions C L (01:03:49)
- a set locations V a set variables a set of input signals (01:03:49)
- 2 Timed Semantics (01:10:07)
- In between the instantaneous (01:10:07)
- Use special variables for clocks (01:10:07)
- Basic idea (01:10:07)
- Formal Semantics (01:12:16)
- Be Semantics (01:12:17)
- The set of possible operations and constants is named OP (01:12:17)
- V denotes the set of all conditions over variables of V (01:12:17)
- n and and right hand side bl s of th (01:12:17)
- q V denotes the set of all equations form v (01:12:17)
- 2 Timed Seh1a (01:12:19)
- Formal Semantics (01:12:41)
- B Semantics (01:15:41)
- The set of possible operations and constants is named OP (01:15:41)
- V denotes the set of all conditions over variables of V (01:15:41)
- n and t and right hand side of th (01:15:41)
- Q 6 vi the set of form (01:15:41)
- Simple Blocks (01:17:12)
- Example Block (01:18:32)
- Formal Semantics (01:20:24)
- u 0 is a trace u P 0 is a correct triple of input state and output (01:20:24)
- IR satisfying (01:20:24)
- u Definition A block M is a 7 tuple Vi V F G C X 0 with (01:20:24)
- Composition (01:23:18)
- r Hybrid Semantics (01:23:19)
- Formal Semantics (01:24:22)
- l t p 0 are valid instantaneous transition executions (01:24:22)
- non instantaneous transition block for D l (01:24:22)
- Update and e L For e 6 L we t quire that D 1 (01:24:22)
- 1 e L a continuous model DU (01:24:22)
- Parallel Composition (01:26:41)
- that D 1 l ts well and the internal signal sets 01 0 (01:26:41)
- The M fer ell reachable g (01:26:41)
- as SQ The resulting transition relation is (01:26:41)
- Hybrid ration (01:27:18)
- is otherwise impossible (01:27:18)
- Motivation Re configuration across multiple (01:27:18)
- output variables (01:27:18)
- Also allow changes the sets of input state and (01:27:18)
- Basic idea (01:27:18)
- Formal Semantics (01:28:27)
- inconsistent reconfiguration possible when composing multiple (01:28:27)
- dependent V l ere instead of the location independent V (01:28:27)
- The semantics can by taking into account the location (01:28:27)
- Semantic Problem Zeno Behavior (01:37:37)

Links added to this content

No links have been added to this content so far.

Tags added to this content

No tags have been added to this content so far.

Create Note

Dear user,

with the manuscript function you'll be able to create your own digital lecture manuscript.

However, in order to link all your notes with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

with the manuscript function you'll be able to create your own digital lecture manuscript.

However, in order to link all your notes with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

Place a Marker

Dear user,

with the marker function you'll be able to create your own digital time markers.

However, in order to link all your markers with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

with the marker function you'll be able to create your own digital time markers.

However, in order to link all your markers with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

Please enable javascript to use this function.

Keyword

Please enable javascript to use this function.

Add to my playlist

Dear user,

with the playlist function you'll be able to create your own lecture video playlists.

However, in order to link all your playlists with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

with the playlist function you'll be able to create your own lecture video playlists.

However, in order to link all your playlists with your user profile it is required that you

login to the tele-TASK portal to use this functionality.

If you don't have an account yet, you may register for a tele-TASK account here.

Playlists

This content is not used in any playlist.