CIS 771, Software Specification, Spring 2018

Classes: MWF, 12:30pm-1:20pm, in Durland 1061.
Instructor: Torben Amtoft, tamtoft hat ksu dot edu, Engineering 2179.
Office Hours: Tuesdays from 1:30pm to 3pm, Thursdays from 3pm to 4:30pm, and by appointment.
Teaching Assistant: Pruthvidhar Dhodda, pdhodda hat ksu dot edu.
Office hours: in DUE 1119/GTA Office, Tuesdays and Thursdays from 9am to 10:30am, and by appointment.
Up-to-date Log File: http://people.cis.ksu.edu/~tamtoft/CIS771/S18/log.html.
This page gives the due dates for all of the assignments in the upcoming weeks. This is to facilitate your planning and time-management.

Reading Material: For the module involving Alloy, we'll use Software Abstractions by Daniel Jackson, published by MIT Press.
For other modules, relevant reading materials will be posted.

Prerequisites:

CIS 301, or familiarity with basic set theory.
We expect that you have had a software engineering course, and have some experience building some non-trivial programs in an object-oriented language.

Learning Outcomes:

The student should become familiar with technologies for software specification and verification that provide deep semantic reasoning about development artifacts such as functional models, architecture, and source-code implementations.

Topics: After a brief introduction, we shall cover

Alloy which brings specifications to life by allowing designers to query constructed models via its constraint analyzer and to easily assess the impact of model refinements.
UML which is the prevalent modeling language in practice, with the robust USE tool providing some useful capabilities for reasoning about OCL enriched UML specifications.
Logika which is an open source pedagogical tool which also serves as a research vehicle for investigating program verification techniques.

Course Organization:

Lectures: Videos, slides and reading material for the course will be made available online. Students are expected to watch the video(s) and cover the slides and reading material on their own.
Lab sessions: Each Wednesday from 12:30-1:20pm, and each Monday from 12:30pm until around 1pm (longer or shorter as the demand may be), we'll meet in classroom 1061 in the Engineering building. This is an opportunity for you to ask questions (so make good use of it!) and for us to find out how your learning is proceeding. Attendance is strongly encouraged but not required.
Off-campus students will not have the benefit of participating in lab discussions, but they will receive copies of any exercises (with solutions) carried out during the lab.
Quizzes: Are given almost every week, usually Tuesday (due one minute before midnight) so they can be discussed at next day's lab session. They carry a total weight of 15% of the course grade.
Assignments: There will be 4 homework assignments during the course, each counting 10% of the total grade.
Assignments that are late will be graded but, unless in case of exceptional circumstances (as defined later), with a penalty of 20 % per day.
Exams: There will be two midterm exams, on February 21st and April 4th, in addition to the final exam on May 8th which is comprehensive but with emphasis on the last part of the course.
All exams are closed book (no material allowed), except for the final where one sheet will be allowed, and together count 45% of the total grade.
Distance students will need to arrange to have a proctor for the exams early in the term. You can arrange for this through K-state Global Campus, or contact the CS department office. Proctors are not needed for the weekly quizzes.

Grading: Final letter grades are not based on strict percentage cutoffs but are "curved" by taking into account the difficulty of the exercises and exams. As a rule of thumb, however, you should expect that to earn an A it requires at least 85% total, and at least 75% for the exams, and to earn a B it requires at least 70% total, and at least 60% for the exams. In general, my approach to grading is expressed well by this piece by S.A. Miller.

An incomplete (I) final grade will be given only by prior arrangement in exceptional circumstances conforming to departmental policy in which the bulk of course work has been completed in passing fashion.

There will be NO make-up quizzes or exams. Special consideration will be given in only exceptional circumstances, in general limited to:

Emergencies: death in student's immediate family, or near-death experience of the student.
Non-emergencies: certified excused absences for official university activities.

If you believe you qualify for exceptional treatment, you must notify the instructor prior to the date of the quiz or exam to be missed. Under exceptional circumstances, the missing quiz or exam will be ignored when computing the final score; otherwise, the student will get zero.

Computer Access While this course does not involve a lot of programming, it makes significant use of software tools. Many of these can be accessed by you (for free) and installed on your own machine.
If you prefer, we have everything you need on our CS department machines. See the computing systems page for information on how to get an account and use our machines.

Academic Honesty: Kansas State University has an Honor & Integrity System based on personal integrity which is presumed to be sufficient assurance in academic matters one's work is performed honestly and without unauthorized assistance. Undergraduate and graduate students, by registration, acknowledge the jurisdiction of the Honor & Integrity System. The policies and procedures of the Honor System apply to all full and part-time students enrolled in undergraduate and graduate courses on-campus, off-campus, and via distance learning.

A component vital to the Honor & Integrity System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by students. The Honor Pledge is implied, whether or not it is stated: "On my honor, as a student, I have neither given nor received unauthorized aid on this academic work."

A grade of XF can result from a breach of academic honesty. The F indicates failure in the course; the X indicates the reason is an Honor Pledge violation.

For more information, visit the Honor & Integrity System home web page at: www.k-state.edu/honor.

All your graded work must be completed independently. You are very welcome to discuss the course material, as well as specific questions, with your fellow students. However, all submitted answers must be your own work:

You are not allowed to consult previous model solutions that may be around, or solicit the Internet for solutions to specific homework problems.
You are not allowed to show your answers to, or look at the answers of, any other student --- this of course excludes any student that you have been allowed to team up with, but in such a case each of you must be able to understand and explain all parts of the submitted work.

If you are in doubt about what is permissible, please ask me. If collaboration is discovered, students will be reported to the KSU Honor and Integrity program as violating the honors policy.

Students with Disabilities: Students with disabilities who need classroom accommodations, access to technology, or information about emergency building/campus evacuation processes should contact the Student Access Center and/or their instructor. Services are available to students with a wide range of disabilities including, but not limited to, physical disabilities, medical conditions, learning disabilities, attention deficit disorder, depression, and anxiety. If you are a student enrolled in campus/online courses through the Manhattan or Olathe campuses, contact the Student Access Center at accesscenter@k-state.edu, 785-532-6441.

Expectations for Classroom Conduct: All student activities in the University, including this course, are governed by the Student Judicial Conduct Code as outlined in the Student Governing Association By Laws, Article V, Section 3, number 2. Students who engage in behavior that disrupts the learning environment may be asked to leave the class.

Acknowledgment: Most of the course material is adapted from previous courses taught by, among others, John Hatliff and Robby and Venkatash Ranganath.

Copyright as to all lectures. During this course students are prohibited from selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of the professor teaching this course. In addition, students in this class are not authorized to provide class notes or other class-related materials to any other person or entity, other than sharing them directly with another student taking the class for purposes of studying, without prior written permission from the professor teaching this course.

Torben Amtoft