Software Development Methods, Fall 2012

This course introduces a selection of theories and practices that, we believe, will enhance the student's ability in developing correct and high-quality software. Its goal is to acquaint the students with some of the well-used methods and tools for practical software development as well as some fundamentals of software verification, so as to prepare them for a career in software development. The view taken here is that of an engineer (programmer, software engineer, or software architect) and hence the focus of the course is primarily on the technical aspects of software development process.

• 01/10: slides and notes for Hoare Logic available.
• 12/26: slides for Model Checking available.
• 12/15: source code of the Android chatroom example created by Mark Chang; many thanks to Mark.
• 12/12: slides for Formal Logic and OCL and a note on OCL specifications available.
• 11/22: slides for Web Application Security available.
• 11/07: slides for Mobile Application Development on Android available.
• 10/25: the second set of slides for Design Patterns available.
• 10/25: HW#3 due 10/31.
• 10/22: slides for Design Patterns available.
• 10/18: HW#2 due 11/01 11/15 (design document) and 11/08 11/22 (demo).
• 10/18: slides for Eclipse available.
• 10/11: slides for EGit available.
• 10/11: slides for Web Programming available.
• 10/10: slides for Software Development Practices available.
• 10/03: HW#1 due 10/10.
• 09/26: slides for UML Diagrams available.
• 09/26: slides for Invited Talk 1 available.
• 09/20: slides for Design Document and An Example available.
• 09/13: slides for Course Introduction and for An Overview of UML available.
• 08/28: this website is the sole source of all up to date course information and syllabus; there is no separate PDF version.

Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's).

Sean Lee (李建昌, Nexdoor), Dave Lin (林大維, Nexdoor), Jeffrey CH Liu (劉智雄, IBM), Clement CW Su (蘇志文, IBM), Chih-Pin Tai (戴智斌), and Ching-Lin Yu (游景麟, Mozilla).

Thursday 9:10-12:10, Room 204, College of Management, Building 2.

Wednesday 1:20-2:10PM, Room 1108, College of Management, Building 2, or by appointment.

張暐獻, 3366-1205, Xb96705043@ntu.edu.twX (between the enclosing pair of X's).

Object-Oriented Programming and Discrete Mathematics.

Class notes and selected readings.

After an overview of the typical software development process and relevant issues, we will study the UML, several software productivity tools, design patterns, and some fundamental elements of formal software modeling and verification. To practice applying these methods and tools, we will carry out a term project that involves the development of a mobile application. The basics of mobile application development will also be covered in the course.

• Introduction (.5 week: 09/13a)
  Overview of software requirements, development process, design methods, and testing/verification
  [slides]
• Software Modeling: An Overview of UML (.5 week: 09/13b)
  Introduction, basics of modeling, overview of the UML
  [slides]
• Software Development Practice: Design Document (.5 week: 09/20a)
  High level design document, implementation level design document, user story (for Agile)
  [slides; notes: An Example Design Document]
• Invited Industry Talk 1 (.5 week: 09/20b)
  Title: Software Development in Small & Mid-Sized Companies
  Speaker: Dave Lin
  [slides]
• Software Modeling: UML Diagrams (1 week: 09/27)
  Structural modeling (class diagrams, classifiers, interfaces, packages), behavioral modeling (interactions, use case diagrams, interaction diagrams, activity diagrams), architectural modeling (collaborations, deployment diagrams)
  advanced structural modeling (object diagrams, components), advanced behavioral modeling (events, state machines, processes and threads, timing constraints)
  [slides]
• Software Development Practice: Modeling Tools (.5 week: 10/04a)
  RSA, basic UML modeling, conversion between source code and model
• Software Development Practice: Team Collaboration (.5 week: 10/04b)
  • Agile Development Process: Scrum, the Eclipse way, OpenUp
  • Collaboration Tools
    Source Code Version Control: Git
    Project Management, Todo, Issue Tracking: RTC, Trac
    Continuous Integration: RTC, CruiseControl
    [main slides, EGit: Git for Eclipse,Tips for Using Eclipse]
• Mobile Application Development: The Web-Server Side (1 week: 10/11)
  [slides]
• Design Patterns (2 weeks: 10/18, 10/25)
  Why design patterns, introduction to creational, structural, and behavioral patterns, GoF patterns
  [slides, sample code]
  Introduction to enterprise systems, enterprise/cloud computing patterns
  [slides]
• Mobile Application Development: The Android Platform (1 week: 11/01)
  [slides]
• Mobile Application Development: The iOS Platform (1 week: 11/08)
  [slides]
• Software Security: Web Application Security (1 week: 11/22)
  Dynamic Web pages, client-side scripts, security vulnerabilities, vulnerabilities detection and prevention
  [slides]
• Term Project Discussions (1 week: TBD)
  
• Software Modeling: Formal Logic and Correctness Requirements (.5 week: 12/06a)
  Propositions, proofs, theorems, predicates, models
  [slides]
• Software Modeling: OCL (.5 week: 12/06b)
  Object Constraint Language (relation with UML models, values, types, expressions, objects, properties, collection operations)
  [slides; notes: OCL Examples]
• Software Modeling: Alloy (1 week: 12/13)
  Software modeling, simulation, and checking
  [slides]
• Midterm (2012/12/20)
• Software Verification: Model Checking (1 week: 12/27)
  Automata-based model checking, linear temporal logic, Spin (Promela, never-claims), Java PathFinder
  [slides: Automata-Based Model Checking, Temporal Logic and Automata]
• Term Project Presentations (2013/01/03)
• Software Verification: Hoare-Style Verification (1 week: 01/10)
  Axiomatic semantics of programs (assertions, pre/post-conditions, invariants), partial and total correctness, Frama-C, VeriFast
  [slides; notes: Rules of Hoare Logic, Proofs with Hoare Logic]

Homework 10%, Midterm 40%, Term Project 40%, Attendance/Participation 10%.

1. The UML Resource, OMG.
2. The Unified Modeling Language User Guide, 2nd Edition, G. Booch, I. Jacobson, and J. Rumbaugh, Addison-Wesley, 2005.
3. Eclipse, The Eclipse Foundation open source community website.
4. Git.
5. Design Patterns: Elements of Reusable Object-Oriented Software, E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Addison-Wesley, 1995.
6. Android.
7. iOS.
8. The OWASP Website. (Note: a website dedicated to Web application security.)
9. The Formal Methods Page: http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.)
10. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
11. Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (Note: follow the link to author's free download site.)
12. Object Constraint Language, OMG Available Specification, Version 2.0, OMG.
13. Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
14. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer-Verlag, 1995.
15. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzman, Addison-Wesley, 2003.
16. Spin.
17. Java Pathfinder.
18. Verification of Sequential and Concurrent Programs, 3rd Edition, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009.
19. Frama-C.
20. VeriFast.

[Midterm 2004, Solutions]
[Final 2004]
[Midterm 2006, Solutions]
[Final 2006]
[Midterm 2008]
[Midterm 2009]
[Midterm 2010]
[Midterm 2011]