CSE503: Software Engineering

Winter 2002
University of Washington
Department of Computer Science & Engineering

Last updated: Friday, February 15, 2002 09:44 AM

Instructor

Teaching assistant

News and Information

Tentative schedule

 Monday Wednesday Friday
Week 1: January 7-11 Introduction 6-up pdf html Proof of correctness (I) Proof of correctness (II)
Week 2: January 14-18 Requirements/Specifications Algebraic Specifications Model-Based Specifications
Week 3: January 21-25 Holiday: No Class Statechart-based Specifications Model Checking 6-up pdf html
Week 4: January 28-February 1 Analyzing Object Models 6-up pdf html Analysis/Tools (con't from Monday) Design/Architecture 6-up pdf html
Week 5: February 4-8 Design/Architecture Design/Architecture 6-up pdf html Design/Architecture
Week 6: February 11-15 Design/Architecture 6-up pdf html Evolution 6-up pdf html Evolution 6-up pdf html
Week 7: February 18-22 Holiday: No class Evolution Evolution
Week 8: February 25-March 1 Architecture 6-up pdf Architecture 6-up pdf Test/Quality Assurance
Week 9: March 4-8 Test/Quality Assurance Test/Quality Assurance Miscellaneous
Week 10: March 11-15 Miscellaneous Miscellaneous Miscellaneous

Required work

  1. A 10-15 page term paper on a one of the subjects found below (or by negotiation with the instructor and TA) [30%]
    • The objective of this paper is to take the topic, do some added reading and research into it, and provide a scholarly assessment of the state-of-the-art in the area, including open issues.
    • The paper must be written with other members of the class as the intended audience.
    • This must be done alone.  (It's fine to talk to others about the ideas and issues, but the work must be your own.)
    • Possible topics include
      • What is the state of model checking as applied to models extracted automatically from source code?
      • What are the key tradeoffs in the different underlying computational models (e.g., model checking, SAT solvers) for finding counterexamples in Nitpick and the Alcoa systems?
      • What is state-of-the-art in automated theorem provers and/or in proof assistants?
      • What is the state-of-the-art for proofs of program correctness for programs that include [side effects, exceptions, etc. --- pick one or two such language features]?
      • What is the state-of-the-art for proving correctness of object-oriented programs (not "just" abstract data type programs)?
    • Other students are looking at various issues in design patterns, extreme programming, automatic inference of invariants, etc.
    • Here are some model term papers from the first assignment:
  2. A tool evaluation [30%]
    • Choose a tool from our list:
      • Rigi is a reverse-engineering tool that is designed to help programmers understand and reengineer large C programs.
      • "Jinsight is a tool for visualizing and analyzing the execution of Java programs. It may be useful for performance analysis, memory leak diagnosis, debugging, or any task in which you need to better understand what your Java program is really doing."
      • Daikon is a tool for dynamically detecting likely invariants in Java and C/C++ programs.
      • ESC/Java is a tool for finding errors in Java programs. It uses static analysis to find errors such as null dereference errors, array bounds errors, type cast errors, and race conditions at compile time. It supports pre- and post-condition style reasoning.
      • Bandera is a tool for verifying properties of Java programs using model-checking.
      • SLAM is a tool for verifying that clients of an interface use that interface correctly. It looks like SLAM is not currently available, although we could contact people at MSR if someone really wants to use this tool
      • Purify is a tool for detecting memory errors in C/C++ programs at runtime, or debugging garbage-collection related problems in Java. A free trial version of this commercial product is available.
      • NORA/RECS is a tool for restructuring code.
      • Lackwit is a tool that helps programmers with reverse engineering or restructuring tasks. The tool can detect abstraction violations, identify unused variables, functions, and fields of data structures, and detect simple errors of operations on abstract datatypes (such as failure to close after open).
      • Hyper/J is a tool that supports better separation of concerns that cross-cut standard class and method boundaries.
      • Java PathFinder is a model checker for Java programs.
      • Ajax is an infrastructure for building analysis tools. You could apply the built-in analysis tools to programs (finding dead code, checking downcasts for safety, identifying unused fields) or use the infrastructure to build your own code analysis.
      • Splint (formerly LCLint) is a tool for statically checking C programs for security vulnerabilities and coding mistakes.
      • ArchJava is a small extension to Java (developed here at UW!) that lets programmers express the software architecture of a Java program within the source code. The compiler verifies that the code conforms to that architecture.
      • you may request that we allow you to use an alternative tool.
      • Note: we will be vetting these tools to make sure they are reasonably usable; stay tuned
    • Apply the tool to one or more realistic programs with the intent of developing a qualitative assessment of the strengths and weaknesses of the tool.
    • The assessment must be written with other members of the class as the intended audience; it may be written as a document or a web page.
    • This may be done in pairs; students working in pairs share a grade.
    • Here are some model tool evaluation papers from the first assignment:
  3. An extensive project with a significant implementation component [60%]
    • This option requires my permission and explicit agreement on a topic.
    • Only recommended for those with a strong background both in software engineering and in system implementation.
    • This must be done alone.  (It's fine to talk to others about the ideas and issues, but the work must be your own.)

Reading