CIS 890: High Assurance Systems
The course will cover techniques for developing high assurance systems -- systems that are safety critical, security critical, or mission critical in nature. In contrast to general purpose systems, high assurance system development tends to place a more stronger emphasis on rigorous requirements and specifications, verification and validation, risk management, and certification. High assurance system development is more likely to be amenable to and benefit from formal verification techniques -- techniques that use various forms of machine-checkable mathematics or logic to demonstrate that a system satisfies its specification. The goal of this course teach techniques for developing critical software that would usually not be covered in other courses in your computer science degree program. In particular, the course will focus on writing requirements for safety critical systems, formal architecture definition, risk management techniques including various forms of hazard analysis, safety systems, and automated verification. We will aim to illustrate an end-to-end development process for critical systems using examples of varying size.
Note:There is not enough time in the course to cover all topics relevant to safety-critical system development in detail. Topics chosen by the instructor in a particular semester will depend on the instructor's current research activities.
At the end of this course, you should be able to demonstrate the following knowledge and skills:
- Explain basic definitions related to system safety
- Given an overview of the development process for safety-critical systems
- Explain and apply a methodology for writing requirements for safety-critical systems
- Know and apply risk management and hazard analysis techniques such as PHA, FTA, FMECA, STPA
- Use tools for formal architecture and behavior specification relevant to critical systems
- Understand concepts and context relevant to safety-critical systems such as traceability, designing for testing/verification, safety architectures, etc.
- Be familiar with concepts related to system certification, regulation, and application of standards
- Development process and life-cycle for safety-critical systems
- Definitions related to system safety
- Requirements for safety-critical systems
- Formal architectural specifications, behavioral specifications, interface specifications, software contracts
- Risk management techniques, hazard analysis
- Deductive-based verification tools
- Programming languages for safety and security critical software
- Certification and regulatory approval approaches for systems with software
- Assurance cases
In this course, we will study a collection of techniques currently used in industry to design and certify high-assurance systems. We will design and build one or more realistic high-assurance systems, and investigate the extent to which formal verification techniques can be incorporated into our development. This year, our course will include the following project(s):
- Illustrating critical pieces of the development process for safety-critical systems using a Patient-Controlled Analgesic (PCA) Pump.
A PCA Pump is a medical device, often used immediately following surgery, that allows a patient to administer their own pain relief through periodic doses an analgesic such as morphine. The course instructor as well as several students in the course are involved in a number of activities related to PCA pumps including joint projects with engineers as the US FDA to illustrate formal development and verification of medical devices, investigation of hazard analysis and risk management techniques with Underwriters Laboratories, development of integrated medical systems that use PCA pump with researchers at Massachusetts General Hospital, Harvard Medical School, and the Medical Device Plug-and-Play Interoperability Program (MDPnP) at the Center for Integration of Medicine and Innovative Technology (CIMIT), and development of standards for safe interoperability of medical devices. Thus, work done in this course has the potential to support and impact important work in a variety of areas in health care.
For developing the applications listed above, we will use the following tool frameworks that support the development of high assurance systems.
- AADL - Developed by a Society of Automotive Engineers (SAE) sponsored committee of experts, the Architecture Analysis & Design Language (AADL) was approved and published as SAE Standard AS-5506 in November 2004. Version 2 of the standard was published in January 2009. The AADL is designed for the specification, analysis, and automated integration of real-time performance-critical (timing, safety, schedulability, fault tolerant, security, etc.) distributed computer systems. It provides a new vehicle to allow analysis of system designs (and system of systems) prior to development and supports a model-based, model-driven development approach throughout the system life cycle.
- SPARK and Bakar Kiasan - SPARK is one of the premier commercial development frameworks for high-assurance software. The SPARK language is a subset of Ada designed for programming and verifying high assurance applications such as avionics applications certified to DO-178B Level A. It deliberately omits constructs that are difficult to reason about such as dynamically created data, pointers, and exceptions. SPARK includes a procedure annotation language for specifying pre/post-conditions and embedded assertions. Bakar Kiasan is a framework developed by the SAnToS research group at Kansas State for highly-automated checking of SPARK contracts.
- Engineering a Safer World, Nancy Leveson, MIT Press
- Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language (recommended) by Peter H. Feiler and David P. Gluch
- Time: Tuesday & Thursday 2:30 -- 3:45pm
- Place: Durland 1064
- CIS 771: Software Specifications
- Java programming skills
- 3 credits
- John Hatcliff, 2160 Engineering Hall, Office Hours by appointment
Grade Allocation Scheme
- Individual Homework Assignments and Quizzes (25%)
- PodCast Summaries (15%)
- Team Projects (55%)
- Participation (5%)
This course includes both individual assignments and team projects. Individual assignments are expected to be completed "individually" (with no collaboration with other students). For team projects, each student is expected to make a unique and substantial contribution to the assigned project. Expectations for the project will be clarified by constructing a written contract that will summarize scope of the project, expected artifacts along with format and completeness of artifacts to be delivered, role and responsibilities of individual team members. The department does not assign a teaching assistant for this course. Because it will be difficult for the instructor to cover all the grading responsibilities for the course, the assessment mechanisms for the course will involve students in the course critiquing and evaluating work of other students (note that this type of activity will be overseen by the instructor to ensure quality).
Faithful attendance is strongly urged but not required. Part of your total grade for the course is based on your participation in discussions and other classroom activities. Poor attendance in the course will be reflected in the assignment of participation grades.
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: http://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: Any student with a disability that needs a classroom accommodation, access to technology or other assistance in this course should contact Disability Support Services and/or the instructor.
- 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. 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.
- 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.
For a more complete discussion of these issues see the course policies for the College of Engineering at Kansas State University.