OMSE 522 Syllabus 

Winter 2007 (12/06)

Instructor: Cynthia A. Brown

Office: 120-01 FAB

Office Hours: 1-2 Tuesday and Thursday or call 503-725-4036 for an appointment

Course rationale: Software projects often fall short of their goals because the software developed can't be tested or doesn't deliver the features its users actually need. The source of these problems is usually a highly ambiguous or incomplete specification.

What to expect: Explains how abstract models can be used to set the specifications of software systems. Formalized reference specifications serve as a basis for the design of software implementations as well as validating critical properties of software systems. You will learn the fundamental mathematical concepts needed to understand abstract models of software and to reason about them by using examples. (And you thought you'd never use your abstract and applied math skills.)

Course Goals: 

• Understand the importance of formal specifications, and their appropriate use. 

• Learn at least one lightweight formal specification method well enough to use it in real life. 

CRN: 46003, 46004

Textbook: Software Abstractions: Logic, Language, and Analysis, Daniel Jackson, MIT Press 2006, ISBN 0-262-10114-9

Book website: http://softwareabstractions.org

Alloy software website: http://alloy.mit.edu

Additional Reading:

• “No Silver Bullet” by Fred Brooks, available on line at: http://www-inst.eecs.berkeley.edu/~maratb/readings/NoSilverBullet.html

• “Medical Devices: the Therac 25”, from Software, System Safety and Computers, Nancy Leveson, Addison-Wesley 1995. Online at: http://sunnyday.mit.edu/papers/therac.pdf

• The Way of Z, Jonathan Jacky, Cambridge University Press 1996, ISBN 0-521-55976-6 (not required)

Course Mechanics, Policies, and Grading: The course has a WebCT site that all students are expected to access. Your grades will be posted in the course grades area. Some practice projects will be assigned for you to work on in groups. You are very much encouraged to work with each other on these, discuss your ideas and approaches, and check each other’s work. Your grades will be based on other projects that you are expected to work on individually. There may be some quizzes as well, and those are also to be done individually.

I expect that everyone has a laptop they can download the Alloy software onto. If this is not the case, please let me know. You need an odin account (main PSU computer system account) to access the WebCT site. If you don’t have one yet, let me know right away. A lot of this class will involve hands-on exercises getting know Alloy. I hope people will bring their laptops to class, if you are in the face-to-face section, so we can do some in-class exercises. If you are in the online class, there will be an opportunity to interact with the other online students as you do these exercises.