Software Development Methods, Fall 2010
This course introduces a selection of theories, practices, and tools that, we believe, will enhance the student's ability in developing correct and high quality software. 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.
Announcements
Jan. 27: Grade Report available.
Dec. 23: slides for Alloy available.
-
Dec. 09:
HW#2 due on Dec. 16.
Dec. 09: slides and notes for OCL available.
Nov. 10: slides and notes for Hoare Logic available.
Nov. 10: slides for Propositional Logic and First-Order Logic available.
Nov. 10: slides for Behavioral Design Patterns available.
Oct. 21: slides for Structural Design Patterns and Version Control available.
Oct. 20: slides for Design Patterns Introduction and Creational Design Patterns available.
Oct. 06: slides for Software Modeling: Advanced UML (UML Part II) and Web Application Security available.
Sep. 30: slides for Introduction to RTC and Web Application Development and a design document sample available.
Sep. 30: due dates of 1st Preliminary Design Document and 1st Prototype Demo extended to Oct. 20 and Nov. 04 respectively.
-
Sep. 23: slides for Software Modeling: Basic UML (UML Part I) available.
Sep. 19: slides for Formal Logic: A Pragmatic Introduction revised.
Sep. 16: slides for Introduction and Formal Logic: A Pragmatic Introduction and a note on Natural Deduction available.
Sep. 10: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version (unlike in previous years).
Instructor
Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)
Lectures
Thursday 9:10-12:10, Room 101, College of Management, Building I
Office Hours
Wednesday 1:30-2:30PM or by appointment
TA
Ming-Hsien Tsai (蔡明憲), 3366-1205, Xmhtsai208@gmail.comX (between the enclosing pair of X's)
Jen-Feng Shih (施任峰), 3366-1205, Xr98725050@ntu.edu.twX (between the enclosing pair of X's)
Prerequisites
Object-Oriented Programming and Discrete Mathematics
Textbook
Class Notes and Selected Readings
Syllabus/Schedule (with links to slides/notes)
The goal of this course 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. After an overview of the subject matters and a brief glimpse of formal logic, we will study in great detail the UML, design patterns, and some fundamental elements of formal software modeling, verification, and analysis.
Introduction (.5 week: 09/16a)
overview of software requirements, development process, design methods, and testing/verification tools.
[
slides]
Formal Logic: A Pragmatic Introduction (.5 week: 09/16b)
propositions, proofs, predicates, models, theorems
[
slides; notes:
Natural Deduction]
Software Modeling: Basic UML (1 week: 09/23)
introduction, basics of modeling, overview of the UML, structural modeling (
class diagrams, classifiers, interfaces, packages), behavioral modeling (
interactions, use case diagrams, interaction diagrams, activity diagrams), architectural modeling (
collaborations, deployment diagrams)
[
slides]
-
Software Modeling: Advanced UML (.5 week: 10/07a)
advanced structural modeling (
object diagrams, components), advanced behavioral modeling (
events, state machines, processes and threads, timing constraints)
[
slides]
Software Security (.5 week: 10/07b)
dynamic Web pages, client-side scripts, frameworks, security vulnerabilities, vulnerabilities detection and prevention
[
slides]
-
Design Patterns: Structural Patterns (1 week: 10/21)
Guest Lecturer: Jeffrey CH Liu, IBM
adapter, bridge, composite, flyweight, proxy, decorator, facade
[slides:
Structural Patterns;
Version Control]
Formal Logic: Propositional and First-Order Logics (1.5 weeks: 10/28, 11/11a)
satisfiability, tautologies, validity, deduction/proofs, soundness, completeness
[slides:
Propositional Logic,
First-Order Logic]
Design Patterns: Behavioral Patterns (1 week: 11/04)
Guest Lecturer: Jim CL Yu, IBM
chain of responsibility, iterator, observer, mediator, command, memento, state, strategy, template method, interpreter, visitor
[
slides]
-
Software Modeling: OCL (1 week: 11/25)
Object Constraint Language (
relation with UML models, values, types, expressions, objects, properties, collection operations)
[
slides; notes:
OCL Examples]
Software Modeling: Alloy (1 week: 12/02)
software modeling, simulation, and checking
[
slides]
Software Modeling: Event-B (1 week: 12/09)
Guest Lecturer: Prof. Jean-Raymond Abrial
(cancelled)
Midterm (2010/12/16)
Software Verification: Hoare-Style Verifiers (2 weeks: 12/23, 12/30)
Frama-C, Spec#
Term Project Presentations (2011/01/06)
-
Grading
Homework 20%, Midterm 40%, Term Project 40%.
References
Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (free!)
Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
-
The Unified Modeling Language User Guide, 2nd Edition, G. Booch, I. Jacobson, and J. Rumbaugh, Addison-Wesley, 2005.
Object Constraint Language, OMG Available Specification, Version 2.0,
OMG.
Design Patterns: Elements of Reusable Object-Oriented Software, E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Addison-Wesley, 1995.
Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
Modeling in Event-B: System and Software Engineering, J.-R. Abrial, Cambridge University Press, 2010.
The SPIN Model Checker: Primer and Reference Manual, G.J. Holzman, Addison-Wesley, 2003.
-
Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer-Verlag, 1995.
-
Old Exams and Solutions