CompSys705

Mathematical techiniques applied to embedded and software systems.  Lecturers seem to be lenient and flexible with the course work. Model checking occurs over the whole state space but this is a big problem when the state space explodes due to the product automata. Explicit state model checking is a searching procedure where you backtrack and see if you have reached an outcome; reachability analysis.

Binary decision diagram - data structures for Boolean function manipulation. States encoded as BBD and modelled checked - symbolic model checking.

Design/property verification checks that the model behaves to specifications and satisfies the temporal logic. Implementation checks that the resulting implementation on hardware or software is equivalent to the model that it is based on.

Simulation/testing may be used to show the presence of errors and verification proves the absence of certain errors. Verification shouldn't replace simulation as there us a large range of properties to prove.

CCS: calculus of communicating systems.
CSP: communicating sequential processes.

CCS operators. Interleaved parallel used for parallel composition. Interleaved parallelism is non-deterministic because you do not know ahead of time what sequence will be taken. If you have to wait for the outcome then it is not possible to predict what will happen.

Homework: function, relation, partial function, injective, bijective, surjective function, partially ordered set, totally order set, lattices.

Sent from my iPod Touch