Synopsis: This course will expose students to formal specification methods, with a particular focus on those used in software architectures. A secondary focus of the class will be on the many software development activities, including architecture, that benefit from the use of formal methods. Several categories of formal methods will be studied, including algebraic, axiomatic, model-based, state-based, and temporal. Specific modeling formalisms within each category will be highlighted and their applicability to software architectures assessed. Students will study different types of formal specification languages and utilize specific languages to describe software systems.