| 10 september 2012 | 1.
Introduction to software design I) Presentation of the course Slides II) History of software design Slides III) Life cycle of a software Slides 1) Steps
IV) Discussion about the projecta) Requirements
analysis, UML use case diagrams
2) Life cycle modelsb) Analysis of the domain, UML class diagram and UML sequence diagram c) Design, design by contract f) Implementation g) Verification (tests, model-checking, proof assistant) a) V-model
b) Spiral model UML pictionary game (pdf + source) |
TD1 |
| 17 september 2012 | 2.
Analysis of the domain Example: a flight reservation system Slides 3. Object design Slides I) Symptoms of a rotting system II) Good principles 1) Principles of
object oriented class design
III) Projects: 2 groups (Pong and UML editor)
2) Principles of package architecture |
TD2 |
| 24 september 2012 | IV). Design
patterns Slides 1) Creation
2) Structural 3) Behaviour |
|
| 1 october 2012 | 4.
UML and logic I) Motivation for reasoning on UML class diagram a) Infering
informations
II) First order logicb) Generate UML object diagrams a) Syntax
II) UML class diagramb) Semantics c) Proofs 1) The whole
picture: the MOF and the approach in logic
IV) The default of first order logic2) Classes 3) Generalisation 4) Association 5) Fields and operations a) The lack of the
finite model property
b) FOL on finite models lacks an axiomatization c) Motivation for finding a decidable logic embedding a fragment of UML |
|
| 8 october 2012 | 5. UML class diagram into modal logic I) Standard motivation for modal logic a) Expressivity
II) Definition of modal logic K (extended with universal modality)b) Decidability a) Syntax
III) Embedding of UML class diagram in an extension of K (namely with
converse and universal modality)b) Semantics c) K and FO a) What do we need?
IV) History of modal logicb) Syntax c) Semantics |
|
| 12 october 2012 | Intermediate report | |
| 15 october 2012 | 6.
Properties of modal logic I) Axiomatization 1) Modal logic K
II) Expressivity2) Moda logic K with converse and universal modality a) Bounded morphism
et bissimulations
b) Traduction standard de la logique modale en premier ordre. Enoncé du théorème de Van Benthem |
|
| 22 october 2012 | 7.
Decidability of modal logic I) Tableau methods 1) Modal logic K
a) Example
b) Tableau rules c) A non-deterministic algorithm 2) K plus converse
and universal modality
II) An optimal algorithm for K plus converse and universal
modality a) Non-terminaison
|
|
| 5 november 2012 |
b) Loop-test
(inclusion test and equality test)
c) Application: generating UML object diagram d) In practice e) A theoretical
algorithm based on Hintikka sets
8.
Complexity theoryI) Turing machine a) Definition
II) Complexity in timeb) Tilings a) Tilings
of squares
III) Complexity in spaceb) SAT a) Tiling of a
corridor
|
|
| 12 november |
b) QBF and Savitch's
theorem
9.
AlternationI) Motivation: EXPTIME II) Alternating Turing machine III) Comparison of complexity classes: AP = PSPACE and APSPACE = EXPTIME IV) Hardness and UML class diagram |
|
| 26 november | 10. Introduction to software
verification I) Sadness Rice's theorem
II) Fight against undecidabilitya) Peer reviews
b) Tests - unit testing
c) Proof assistant- integration testing : stub and feeback arc set problem d) Model checking demo with Java Path Finder 11. Introduction to model checking I) From programs to non deterministic models 1) Concurrency: non determinism from interleaving II) Expressing properties2) Statechart: non determinism from the environment/user 3) Programs with complex data: non determinism from abstraction 1) Standard properties (safety, liveness, fairness) 2) The CTL* language - syntax |
|
| 3 december | - semantics- LTL, CTL fragments III) Model checking of a CTL formula12. Path properties I) Model checking of LTL is PSPACE-hard II) Model checking reduces to SAT |
|
| 4 december, 1:30pm | Presentation of the two projects | |
| 4 december, 3:30pm |
III) LTL satisfiability problem is in PSPACE
12. Expressiveness of temporal logics I) LTL is better than CTL II) CTL is better than LTL 13. Some remarks about BDD |