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.
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.
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.
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.
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.
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.
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.