This shows you the differences between two versions of the page.
courses:sdm2020:main [2020/04/29 16:39] tsay2 [Announcements] |
courses:sdm2020:main [2020/07/26 11:38] (current) tsay2 [Announcements] |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * 07/03: grade report available; contact the instructor Yih-Kuen Tsay by 5PM 07/04 if you have any question or request. | ||
+ | * 06/24: slides for Hoare Logic available. | ||
+ | * 06/03: slides for Logic and OCL available. | ||
+ | * 05/27: slides for Software Testing available. | ||
+ | * 05/20: {{courses:sdm2020:hw4.pdf|HW#4}} due 05/27. | ||
+ | * 05/20: Review forms for the second preliminary demo presentations: {{courses:sdm2020:Presentations_demo2.docx|Evaluation by Individual Reviewer}} and {{courses:sdm2020:Presentations_demo2_comments.docx|Team-for-Team Comments}}. | ||
+ | * 05/20: slides for Web Application Security available. | ||
+ | * 05/06: slides for Design Patterns and some code examples available. | ||
+ | * 04/29: slides for Design Document and an example design document available. | ||
+ | * 04/29: slides for Agile Development in Practice available. | ||
* 04/29: {{courses:sdm2020:hw3.pdf|HW#3}} due 2:10PM 05/06. | * 04/29: {{courses:sdm2020:hw3.pdf|HW#3}} due 2:10PM 05/06. | ||
* 04/29: Review forms for the first preliminary demo presentations: {{courses:sdm2020:Presentations_demo1.docx|Evaluation by Individual Reviewer}} and {{courses:sdm2020:Presentations_demo1_comments.docx|Team-for-Team Comments}}. | * 04/29: Review forms for the first preliminary demo presentations: {{courses:sdm2020:Presentations_demo1.docx|Evaluation by Individual Reviewer}} and {{courses:sdm2020:Presentations_demo1_comments.docx|Team-for-Team Comments}}. | ||
Line 60: | Line 70: | ||
* **Software Implementation: Web Programming Pearls** (1 week: 03/25) [{{courses:sdm2020:WebProgrammingBasics.pptx|basics}}, {{courses:sdm2020:WebProgrammingAdvanced.pptx|advanced}},{{courses:sdm2020:examples.zip|examples}}] | * **Software Implementation: Web Programming Pearls** (1 week: 03/25) [{{courses:sdm2020:WebProgrammingBasics.pptx|basics}}, {{courses:sdm2020:WebProgrammingAdvanced.pptx|advanced}},{{courses:sdm2020:examples.zip|examples}}] | ||
* **Term Project: Proposal Presentations** (1/3 week: 04/01a) \\ | * **Term Project: Proposal Presentations** (1/3 week: 04/01a) \\ | ||
- | * **Invited Talk** (or Make-Up Lecture) (2/3 week: 04/01b) \\ [{{courses:sdm2020:invitedtalk_softwaredevelopment.pdf|slides}}] | + | * **Invited Talk** (or Make-Up Lecture) (2/3 week: 04/01b) |
- | * **Software Modeling: Domain Modeling** (2 weeks: 04/08, 04/15) \\ What and how (abstract models, notations and constructs, basic business logics, crossing domains, layers of abstraction), common patterns, with group exercises and discussions \\ [{{courses:sdm2020:domainmodel.pptx|slides}},{{courses:sdm2020:domainmodel_appendix.pptx|appendix}}] | + | * **Software Modeling: Domain Modeling** (2 weeks: 04/08, 04/15) \\ What and how (abstract models, notations and constructs, basic business logics, crossing domains, layers of abstraction), common patterns, with group exercises and discussions \\ [{{courses:sdm2020:domainmodel.pptx|slides}}, {{courses:sdm2020:domainmodel_appendix.pptx|appendix}}] |
* **Software Development Practice: Agile Development in Practice** (1 week: 04/22) \\ Principles for building an agile team, essentials of scrum, kanban, and scrumban, DevOps, and engineering culture\\ [{{courses:sdm2020:Agile.pdf|slides}}] | * **Software Development Practice: Agile Development in Practice** (1 week: 04/22) \\ Principles for building an agile team, essentials of scrum, kanban, and scrumban, DevOps, and engineering culture\\ [{{courses:sdm2020:Agile.pdf|slides}}] | ||
* **Term Project: First Preliminary Demos** (1/3 week: 04/29a) \\ | * **Term Project: First Preliminary Demos** (1/3 week: 04/29a) \\ | ||
- | * **Software Development Practice: Design Document** (2/3 week: 04/29b) \\ High level design document, implementation level design document, user story (for Agile) \\ [{{courses:sdm2020:DesignDocIntroduction.pdf|slides}}, notes: {{courses:sdm2020:DesignDocSimpleExample.doc|An Example Design Document}}] | + | * **Software Development Practice: Design Document** (2/3 week: 04/29b) \\ High level design document, implementation level design document, user story (for Agile) \\ [{{courses:sdm2020:DesignDocIntroduction.pdf|slides}}, {{courses:sdm2020:DesignDocSimpleExample.doc|An Example Design Document}}] |
- | * **Design Patterns** (2 weeks: 05/06, 05/13) \\ Why design patterns, introduction to creational, structural, and behavioral patterns, GoF patterns \\ [{{courses:sdm2020:DesignPatterns.pdf|slides}}; {{courses:sdm2020:DesignPatternsExamples.zip|code examples}}] | + | * **Design Patterns** (2 weeks: 05/06, 05/13) \\ Why design patterns, introduction to creational, structural, and behavioral patterns, GoF patterns \\ [{{https://docs.google.com/presentation/d/1J3RuDik3KMP-PpPbjxZo5MCg7t9i-ZSQ67titjHldqc/edit#slide=id.p|slides}}, {{courses:sdm2020:DesignPatternsExamples.zip|code examples}}] |
* **Term Project: Second Preliminary Demos** (1/3 week: 05/20a) \\ | * **Term Project: Second Preliminary Demos** (1/3 week: 05/20a) \\ | ||
* **Software Security: Web Application Security** (2/3 week: 05/20b) \\ Dynamic Web pages, client-side scripts, security vulnerabilities, vulnerabilities detection and prevention \\ [{{courses:sdm2020:web_app_security.pptx|slides}}] | * **Software Security: Web Application Security** (2/3 week: 05/20b) \\ Dynamic Web pages, client-side scripts, security vulnerabilities, vulnerabilities detection and prevention \\ [{{courses:sdm2020:web_app_security.pptx|slides}}] | ||
Line 72: | Line 82: | ||
* **Term Project: Final Presentations (2020/06/10)** | * **Term Project: Final Presentations (2020/06/10)** | ||
* **Final Exam (2020/06/17)** | * **Final Exam (2020/06/17)** | ||
- | * **Software Verification: Formal Verification** (2 weeks: 06/24, 07/01) \\ Automata-based model checking, linear temporal logic, Spin (//Promela, never-claims//) \\ [{{courses:sdm2020:automata_based_model_checking.pdf|slides}}]\\ Axiomatic semantics of programs (//assertions, pre/post-conditions, invariants//), partial and total correctness \\ [{{courses:sdm2020:hoare_logic.pdf|slides}}] | + | * **Software Verification: Formal Verification** (2 weeks: 06/24, 07/01)\\ Axiomatic semantics of programs (//assertions, pre/post-conditions, invariants//), partial and total correctness \\ [{{courses:sdm2020:hoare_logic.pdf|slides}}, notes: {{courses:sdm2020:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:sdm2020:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}] \\ Automata-based model checking, linear temporal logic, Spin (//Promela, never-claims//) \\ [{{courses:sdm2020:automata_based_model_checking.pdf|slides}}] |
===== Grading ===== | ===== Grading ===== | ||
Line 96: | Line 106: | ||
- //Object Constraint Language, OMG Available Specification, Version 2.0//, OMG. | - //Object Constraint Language, OMG Available Specification, Version 2.0//, OMG. | ||
- //Software Abstractions: Logic, Language, and Analysis//, D. Jackson, MIT Press, 2006. | - //Software Abstractions: Logic, Language, and Analysis//, D. Jackson, MIT Press, 2006. | ||
+ | - //Verification of Sequential and Concurrent Programs, 3rd Edition//, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009. | ||
+ | - [[http://frama-c.com/|Frama-C]]. | ||
+ | - [[http://people.cs.kuleuven.be/~bart.jacobs/verifast/|VeriFast]]. | ||
- //Temporal Verification of Reactive Systems: Safety//, Z. Manna and A. Pnueli, Springer-Verlag, 1995. | - //Temporal Verification of Reactive Systems: Safety//, Z. Manna and A. Pnueli, Springer-Verlag, 1995. | ||
- //The SPIN Model Checker: Primer and Reference Manual//, G.J. Holzman, Addison-Wesley, 2003. | - //The SPIN Model Checker: Primer and Reference Manual//, G.J. Holzman, Addison-Wesley, 2003. | ||
- [[http://spinroot.com/|Spin]]. | - [[http://spinroot.com/|Spin]]. | ||
- [[http://babelfish.arc.nasa.gov/trac/jpf|Java Pathfinder]]. | - [[http://babelfish.arc.nasa.gov/trac/jpf|Java Pathfinder]]. | ||
- | - //Verification of Sequential and Concurrent Programs, 3rd Edition//, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009. | ||
- | - [[http://frama-c.com/|Frama-C]]. | ||
- | - [[http://people.cs.kuleuven.be/~bart.jacobs/verifast/|VeriFast]]. | ||
===== Old Exams and Solutions ===== | ===== Old Exams and Solutions ===== |