Reading

You will be reading several papers that provide different perspectives on software specifications and other papers that will help you learn how to use tools associated with specification approaches.

• Hints to Specifiers, Jeannette Wing, July, 1995.
• Formal Specification: a Roadmap, by Axel van Lamsweerde, in Future of Software Engineering (Limerick, Ireland). June, 2000. ACM Press.
• Alloy
  • Alloy : A Lightweight Object Modelling Notation by Daniel Jackson, Nov, 2001.
  • COM Revisited: Tool Assisted Modelling and Analysis of Software Structures by Daniel Jackson and Kevin Sullivan, in Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000.
  • A Comparison of Object Modelling Notations : Alloy, UML and Z by Daniel Jackson, August, 1999.
• UML/USE
  • Excerpts from the UML 1.3 Specification on Class Diagrams
  • Excerpts from the UML 1.3 Specification on Statechart Diagrams
  • Excerpts from the UML 1.3 Specification on Object Constraint Language
  • OCL - Syntax, Semantics and Tools , Richters and Gogolla.
  • Validating UML Models and OCL Constraints, Richters and Gogolla.
• Extended Static Checking for Java
  • Extended Static Checking (ESC) (index of several document formats)
  • ESC/Java User's Manual (html)

Daily life

• Weekly Objectives -- tasks that you should be able to perform as the course progresses
• Weekly Quizzes -- short graded quizzes given in lab sections
• Weekly Exercises -- ungraded exercises (corresponding to potential exam questions)
• Weekly Explorations -- other interesting resources related to the course and lectures
• Lecture Examples -- sources for Alloy, USE, and ESC-Java examples used in lectures
• Homework -- links to the discriptions and solutions of graded homeworks

Tool Home Pages

Below are the home pages for the tools that will use in the course. Each of these tools is available for windows, linux or solaris platforms. We will have versions of solaris executable on the K-state CIS machines made available. If you want your own copy just download and install (its pretty easy).

• Alloy and its Constraint Analyzer are an object modeling language and analysis tool, respectively. Note: we are using the OLD version of Alloy, i.e., Alloy Alpha 1.1, this semester. The new version has lots to offer, but its documentation isn't as mature as the previous version.. It is available for windows machines here.
• USE USE is a UML-based tool that processes class diagrams and OCL specifications. Models conforming to the class diagrams can be animated and automatically checked against the given OCL specifications.
• ESC/Java is a tool that uses a theorem prover to automatically check code-level specifications written in the JML specification language.

In the following red means that laboratory sections will meet and blue means there is no meeting.

PDF versions of the slides for the lectures and the video lecture's will be linked directly from this page. They are also available directly from K-state Online; to access them you will need a K-state Online account (just signup at their web-site as long as you are registered for this course). Technical problems in accessing or displaying the online lectures can be resolved through K-state Online's help desk:

• Web: http://online.ksu.edu/support
• Email: help@online.ksu.edu
• Phone: (800) 865-6143 or (785) 532-0198

We reserve the right to adjust this schedule based on the interest that the class shows in different topics.