Syllabus
CIS 771 Software Specifications -- Course Syllabus
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
SPARK with Bakar Kiasan
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.
We are covering aspects of UML due to its current popularity. The USE tool is robust and provides some useful capabilities for reasoning about OCL enriched UML specifications. We believe that students may well use a tool like USE in their design/development work in the future.
We are including a module on SPARK and the Bakar Kiasan specification checking tool because they enable code-level specifications. The fact that SPARK 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 (SPARK).
Course Organization: Weekly Lecture & Laboratory
This course is divided into lecture and laboratory, given on Tuesdays and Thursdays, respectively:
Lecture: videos, slides and reading material for the course will be made available online at the beginning of each week. Students are expected to watch the video(s) and cover the slides and reading material on their own.
Laboratory: A weekly laboratory section will be held on-campus in Nichols 019. Laboratory meetings provide you with an opportunity for asking questions, so make good 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 or through K-State Online. The quizzes are designed to take approximately 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
Teaching Assistant
- Rohit Parimi, Office: Nichols 237, Office Hours: M W 11:30 - 12:30, Phone: 785-532-7860
Marking Scheme
(Subject to adjustments.)
40% - Homework 4 x 10%
15% - Quizzes, each quiz worth 1-2%, though generally 2%
20% - Mid-term Exam
25% - Final Exam
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.
Distance students will need to arrange to have a proctor for both the mid-term exam and the final early in the term by contacting DCE (and CC me). You can arrange for this through K-state DCE, or contact the CIS department office. Proctors are not needed the weekly quizzes.
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. Under exceptional circumstances, the quiz or exam weight will be added to the final exam weight; otherwise, the student will get zero for the missed quiz or exam.
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
There is no standard relationship between percentages and letter grades assigned for this course, though generally speaking, the following ranges are common:
A: 90% -- 100%
B: 80% -- 89%
C: 70% -- 79%
D: 60% -- 69%
F: below 60%
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 encouraged but not required.
Statement Regarding Academic Honesty
Kansas State University has an Honor 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 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. The honor system website can be reach via the following URL: www.ksu.edu/honor.
A component vital to the Honor 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.
Other Administrative Issues
Incompletenes: 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.
Students with Disabilities: If you have any physical or learning disability which will make it difficult for you to carry out the work as I have outlined in this syllabus or which will require academic accommodations, please notify me the first two weeks of the course.
Harrassment: One purpose of your education is to help you develop skills, approaches, and abilities that are necessary for effective teamwork, and for your success in your profession and as a citizen. It is important that you understand your rights and responsibilities regarding the University's Sexual and Racial Harassment policies (full text of the policies can be found on KSU's web site at http://www.ksu.edu/uauc/fhbook/fhxj.html). If you experience any situations, in or out of class, that seem inappropriate or that make you uncomfortable, a list of resources and courses of action to assist you can be found on the College of Engineering web site at http://www.engg.ksu.edu/harassment-statement.
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 Government Association By Laws, Article VI, Section 3, number 2. Students that engage in behavior that disrupts the learning environment may be asked to leave the class.
Campus Safety: Kansas State University is committed to providing a safe teaching and learning environment for student and faculty members. In order to enhance your safety in the unlikely case of a campus emergency make sure that you know where and how to quickly exit your classroom and how to follow any emergency directives. To view additional campus emergency information go to the University's main page, www.k-state.edu, and click on the Emergency Information button.
Copyright Issues: Class and lecture notes for this course carry a copyright. Students are prohibited from selling (or being paid for taking) notes during this course to or by any person or commercial firm without the express written permission of the professor teaching this course.
For a more complete discussion of these issues see Course Policies for the College of Engineering at Kansas State University.
