17-651 Models of Software Systems
12 units, Carnegie Mellon University
Scientific foundations for software engineering depend on the use of precise, abstract models for describing and reasoning about properties of software systems. This course considers a variety of standard models for representing sequential and concurrent systems, such as state machines, algebras, and traces. It shows how different logics can be used to specify properties of systems, such as functional correctness, deadlock freedom, and internal consistency. Concepts such as compositionality, abstraction, invariants, nondeterminism, and inductive definitions are recurrent themes throughout the course. After completing this course, students will 1. Understand the strengths and weaknesses of certain models and logics including state machines, algebraic and process models, and temporal logic 2. Be able to select and describe appropriate abstract formal models for certain classes of systems, describe abstraction relations between different levels of description, and reason about the correctness of refinements 3. Be able to prove elementary properties about systems described by the models introduced in the course and 4. Understand some of the strengths and weakness of formal automated reasoning tools. Prerequisites Undergraduate discrete math including firstorder logic, sets, functions, relations, and simple proof techniques such as induction. Sections D, PP and G are NOT available for oncampus students. Admission to the class is by approval from the instructor If you are not MSEMSITSEMITS, send email to garlancs.cmu.edu for permission to enroll. The email should briefly describe your background, whether you have taken an undergraduate discrete math course, and why you would like to take the course. The course must be taken for a letter grade not passfail. This is a graduate level course.
Prerequisites: none listed
Courseweave needs JavaScript to show sections, workloads and planning tools.