Trust Assessment

Assessment of the trustworthy features of a system is key to the process of developing trustworthy systems. The courses on this roadmap will teach you the tools to verify systems directly, e.g., via proofs of correctness, or indirectly, e.g., via modeling and simulation.

Courses

AE 498 SSS: Software and Systems Safety

Learn to design a safety-critical software decision aid for an instrumented landing system parallel runway approach for large aircraft. Course will cover the entire software life cycle, including preliminary hazard analysis techniques, requirements specification, formal modeling, software design specification/code generation, testing, verification and validation, and human-machine interface design. Students will be divided into design teams and given deliverables for each stage of the design process. At the end of the course, a formal design review will be conducted on the developed decision aid, along with a "testing competition" using actual air traffic management data.

CS 476: Program Verification

Examines formal methods for demonstrating correctness and other properties of programs; includes an overview of predicate calculus. Topics include: invariant assertions, Hoare axiomatics, well-founded orderings for proving termination, structural induction, computational induction, data structures, and parallel programs. Prerequisites are CS 225 and either CS 373 or MATH 414. Available in Fall 2012.

CS/ECE 541: Computer Systems Analysis

Development of analytical models of computer systems and application of such models to performance evaluation; topics include scheduling policies, paging algorithms, multiprogrammed resource management, and queuing theory. Prerequisite is ECE 313, MATH 461, or MATH 463. Available in Fall 2012.

CS 598DM: Software Testing and Analysis

The focus of the course is on analysis of code, but it also covers analysis of software models and their use in testing. Students will get familiar with the technical results as well as with the process of doing research in software testing and analysis. The aim is to help students start research in this field or apply its results in their ongoing research.

ECE 498DN: Discrete Event Simulation of Computer and Communication Systems

This course focuses on methodologies and techniques for the simulation-based analysis of computer and communication systems. It covers statistical issues of input modeling and output analysis, as well as algorithmic techniques for achieving high performance.

ECE 598 SV: Automatic Approaches to Hardware and Software Verification

This course will introduce the student to formal verification techniques to check hardware designs and embedded software. The course will present an overview of the verification paradigms that are most applied in practical hardware and embedded system verification. The course will discuss state-space-based automatic verification techniques and deductive checking techniques. There will be an emphasis on the practical ramifications of these algorithms in contemporary semiconductor as well as embedded software environments. Prerequisites are ECE 411 or CS/ECE 462 and CS 273 or CS 225 or consent of instructor.