課程大綱：系統驗證：自動機和行為等效培訓
Behavioural modelling
System Validation is the field that studies the fundamentals of system communication and information processing.
It allows automated analysis based on behavioural models of a system to see if a system works correctly.
We want to guarantee that the systems does exactly what it is supposed to do. The techniques put forward
in system validaton allow to prove the absence of errors. It allows to design embedded system behaviour that
is structurally sound and as a side effect enforces you to make the behaviour simple and insightful.
This means that the systems are not only behaving correctly, but are also much easier
to maintain and adapt.’Automata and behavioural equivalences' shows you how to look at system behaviour as state machines.
It discusses behavioural equivalences and illustrate these in a number of examples and quizzes.
This module introduces automata or labelled transition systems as the basic way to model the behaviour
of software controlled systems. It subsequently addresses the question
when such behaviours are equivalent.Reading material. J.F. Groote and M.R. Mousavi.
Modeling and analysis of communicating systems. The MIT Press,
Basic behavioural equivalences
This module shows the most important equivalences that express when
the behaviour of two automata can be considered to be equivalent.
It will become obvious that there are multiple of such notions, all fit for use under different circumstances.
Furthermore, the all-important notion of the internal or hidden action
is introduced with some associated behavioural equivalences.
More behavioural equivalences
This module elaborates on the equivalences provided earlier.
It is shown how it can be applied, especially to the alternating bit protocol.
Furthermore, a number of additional equivalences are introduced.
加入高級會員獲得助教答疑
