Embedded distributed system design principles stemming from behavioral formal specifications. Reactive systems and real-time systems: abstraction level, similarities and differencies. Reactive system and real-time system models: state sequences and trees, timed-state sequences; Kripke structures. Basic logical properties: fairness, livness, safety, feasibility; real-time livness, bounded time response. Modal logics and temporal logics: Kripke semantics. Temporal logic fundamentals: syntax, semantics, axiomatics. Time models and temporal logics: order, future x past, discrete x dense x continuous, time origin, time end. LTL. CTL. Temporal logic and real time: observation sequences; approach by Alur and Henzinger; approach by Koymans and Vytopil and de Roever; approach by Pnueli and de Roever. Formal specifications of embedded systems. Provers. Model checking. Real-time systems verification. Case studies.

Questions:

1. Discrete systems theories: transformational, reactive and RT
2. State sequence model of discrete systems behavior - properties: fairness, livness, safety
3. Meanings and representation of the term "time"
4. Timed-state sequence representation of the RT system behavior - properties: RT livness (non-Zeno behavior), feasibility (machine closure), bounded response
5. Time in distributed systems: a) Lamport model, logic clocks, physical clocks
6. Modal and temporal logics, Kripke semantics
7. Traditional proposition temporal logic, axiomatic base, its soundness and completness
8. Proving and model checking
9. Time models and propositional temporal logics
10. RT extensions of temporal logic