Purpose

In the future, everything will be smart. Microchips will be embedded in most man-made devices, from clothing to appliances, from vehicles to buildings. A variety of networks will connect these devices. The world will become one large distributed computer. And software will control it all. Billions of lives and trillions of dollars already depend on the correct operation of software, and the degree of automation is likely to increase. More safety critical processes will be controlled by software, and most commerce is expected to be electronic. As networks increase connectivity, the interaction of distributed embedded computers will provide unprecedented capabilities, but also great complexity.

In this brave new world you will be building software that must operate as expected. If it does not the consequences will be great (to you and society).

How can we possibly construct enormously complex systems built from parts that are themselves built by hundreds of people and have any hope that they will work?

In this course, we will study a collection of techniques that lie at the foundation of an approach to software development that can enable the construction of large highly reliable software. That foundation is specification of the precise meaning of the execution behavior of software.

The old argument for precise specification still holds: Without a precise specification of what we want to build:

• we can't tell that we're building the right thing
  
• we can't tell if the program we built does what we want

More importantly, as we will see in this course, precise specification allows for the construction of automated tools that can perform a kind of testing of our specifications to find bugs in requirements, designs, and code. Far from being removed from practice, formal specification holds the key for developing the next generation of tools that will sit alongside debuggers, simulators, and testing tools in the modern developers toolkit.

This course is dedicated to teaching the principles and application of the following tool-supported formal specification methods:

• Alloy
  
• USE
  
• JML

We have chosen these methods because we believe that the most effective formal specification methods are those that also provide some form of automated tool support.

Alloy, in particular, brings specifications to life by allowing designers to query constructed models via its constraint analyzer and to easily assess the impact of model refinements. In addition, Alloy has a readable graphical and textual notation and it has a very small and semantically clean core language. We believe that all these factors make it an excellent pedagogical vehicle and a tool that can be applied to realistic problems with a fairly large return on the analyst's effort. (Note: In previous semesters, we used an older version of Alloy. This semester, we will be using the most recent version of Alloy.)

We are covering aspects of UML due to its current popularity. The USE tool is very robust and provides some very useful capabilities for reasoning about OCL enriched UML specifications. We believe that students may well use this tool in their design/development work in the future.

We are including a module on the Java Modeling Language (JML) and the Kiasan JML specification checking tool because we wanted to include a discussion of code-level specifications. The fact that JML has associated with it several different forms of automated tool support is in line with our preference for tool-supported methods.

In summary, these methods span the development process ranging from high-level semantic modeling (Alloy), to system architecture design (USE), to coding and debugging (JML).

Schedule

Lecture: Lectures for the course will be made available online at the beginning of each week. Students are expected to watch the lectures on their own.

Laboratory: A weekly laboratory section will be held on-campus Thursdays from 9:30 am - 10:45 am in Nichols 127. Laboratory meetings provide your opportunity for asking questions so make use of it. Laboratory meetings provide us with an opportunity for finding out how your learning is proceeding; quizzes will be given each week.

Off-campus students, will not have the benefit of participating in lab discussions, but they will receive copies of the exercises carried out during the lab (with solutions).

Off-campus students will receive the weekly quizzes via email. The quizzes are designed to take around 20 minutes. Off campus students will typically receive 24 hours to complete and return the quiz. All quizzes will be closed book/notes and must be completed independently.

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.

Credits

• 3 credits

Instructor

• Robby (robby@cis.ksu.edu)
  Nichols 324B
  Office Hours (Online Calendar)

Teaching Assistant

• Scott Harmon (harmon@cis.ksu.edu)
  Nichols 316
  Office Hours: Monday 10:30am-12pm, Wednesday 3pm - 4:30pm
  (Online Calendar)

Marking Scheme

• Homeworks (45%)
  
• Quizzes (20%)
  
• Mid-term Exam (15%)
  
• Final Exam (20%)

A third of your grade will be based on your performance on traditional closed-book, closed notes mid-term and final exams. A fifth of your grade will be based on your performance on weekly quizzes. Nearly half of your grade will be based on assignments related to each of the three specification frameworks that we will be discussing in the course. For Alloy, you will have two assignments:

• a smaller assignment to help you learn the basic properties of the respective framework, and
  
• a larger mini-project to be carried out in conjunction with the case study lectures on the respective framework.

For USE and JML, you will have a single assignment.

Thus, you will have a total of four graded assignments.

Assignments must be completed independently -- no joint work on homework assignments is allowed. If collaboration on homework assignments is discovered, students will be reported to the KSU Honor and Integrity program as a violation of the honors policy. Of course, quizzes and exams must also be completed independently with no interaction between students and without the aid of supplementary materials such as lectures slides, text books, notes, etc.

Off-campus students will need to arrange to have a proctor for both the mid-term exam and the final. You can arrange for this through K-state DCE, or contact the CIS department office. Proctors are not needed the weekly quizzes.

Grading Policy

The course web-page gives the due dates for all of the homework. This is to facilitate your planning and time-management. Given this we expect assignments to be turned in on the due date unless prior arrangements have been made; late assignments receive a reduction of 1% of the total possible points for each hour after the due date/time.

This policy holds for all students in the course (on-campus and off-campus). For off-campus students, late quiz solutions will receive a reduction of 1% of the total possible points for each minute after the due date/time.

To accommodate students who may have the occasional conflict with Lab meetings, we will drop the lowest quiz score in calculating your final grade. If you have to miss two quizzes then one will be dropped but the other will be factored in as a zero.

Grading scale

Course grades are absolute, i.e., there is no curve, and will be calculated based on your overall percentage on assignments as follows:

• A: 90% -- 100%
  
• B: 80% -- 89%
  
• C: 70% -- 79%
  
• D: 60% -- 69%
  
• F: below 60%

There is one additional constraint on your final grade. To receive a letter grade of A, you must achieve at least a B on either the mid-term or final exam. Similarly, to receive a B you must achieve a C, C you must achieve a D on either the final or mid-term exam.

Computer Access

While this course does not involve a lot of programming per se, 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 CIS department machines so you should can get an account on our machines. See the computing systems page for information on how to get an account and use our machines.

Attendance policy

Faithful attendance to all laboratory sections is strongly urged but not required. In general, there will be NO make-up quizzes or exams! Special consideration will be given in only exceptional circumstances. Exceptional circumstances are generally 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.

Other Administrative Issues

• Incompletes:
  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.
  
• Academic Misconduct:
  Plagiarism and cheating are serious offenses and may be punished by failure on the exam, paper or project; failure in the course; and/or expulsion from the university. For more information refer to the ``Academic Conduct'' policy in the Student Life Handbook, which may be found in the KSU Campus Phone Book.
  
• Students with Disabilities:
  If you have any condition, such as a physical or learning disability, which will make it difficult for you to carry out the work as we have outlined it or which will require academic accommodations, please notify me in the first two weeks of the course.

For a more complete discussion of these issues see Course Policies for the College of Engineering at Kansas State University.