General Information

Lecture: 2:00pm - 3:20pm, Tue. & Thu., WH 212 PH 101
Instructor: Dr. Jeff Lei , ylei@cse.uta.edu, 340 NH, 817.272.2341
Office Hours: 1:00pm - 2:00pm, Tue. & Thu.
TA: Wenhua Wang, 10:00 - 11:30am, Mon. & Wed., 239 NH, wenhua.wang@mavs.uta.edu
Class Communication: fmse@listserv.uta.edu

Prerequisite

Basic understanding about software engineering (CSE 5324). Background in first-order logic and automata. A moderate proficiency of the Java language.

Course Description

Software quality is a priority concern of any responsible software development effort. One approach to ensuring software quality is to apply formal methods, i.e., rigorous techniques that have a solid mathematical and logical foundation. In this course, we will study formal methods that can be used to support major software development stages, including requirement specification, software design, and software verification and validation. Examples of the topics covered in this course are Model Driven Architecture (MDA), Design by Contract, Java Modeling Language (JML), Temporal Logic, Buchi Automata, and Model Checking.

Lecture notes will be posted below as they become available.

1/19/2010: Course Admin.
1/21/2010: Introduction
1/26/2010: Logic Review
1/28/2010: Continue on Logic Review
2/2/2010: Program Proof
2/4/2010: Continue on Program Proof
2/9/2010: Introduction to OCL
2/11/2010: No Class
2/16/2010: Project Topics, Evaluation Form
2/18/2010: OCL Expressions
2/23/2010: Continue on OCL Expressions
2/25/2010: Build Models with OCL
2/25/2010: Presentation Schedule
3/2/2010: Continue on Build Models with OCL
3/4/2010: OCL Tools, JML
3/4/2010: HW 1
3/9/2010: Continue on JML
3/11/2010: Continue on JML
3/16/2010: Spring break
3/18/2010: Spring break
3/23/2010: SPIN Overview
3/25/2010: Continue on SPIN Overview
3/30/2010: Continue on SPIN Overview
4/1/2010: Continue on SPIN Overview
4/6/2010: Temporal Logic
4/8/2010: Continue on Temporal Logic
4/13/2010: Search Algorithms
4/15/2010: Continue on Search Algorithms
4/20/2010: Spec #
4/22/2010: ASM
4/27/2010: Z3 (Part I), Z3 (Part II)
4/29/2010: ESC/Java 2
5/4/2010: Java PathFinder 5
5/6/2010: Alloy

Textbook (Recommended)

1. Doron A. Peled. Software Reliability Methods. Springer Verlag, 2001, ISBN:0387951067.
2. Jos Warmer and Anneke Kelppe. The Object Constraint Language. Addison-Wesley,2003, ISBN: 0321179366.
3. Gerard J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2003, ISBN: 0-321-22862-6.

Grading

There will be about five in-class quizzes. The quizzes will consist of true/false, multiple choices, and/or short answer questions. NO makeup quiz will be given. The final grades will be determined according to the following percentages:

Quizzes - 50%
Project/Presentation - 50%

Resources

1. OMG Model Driven Architecture
2. Octopus
3. OCLE
4. USE
5. SPIN

Americans With Disabilities Act

The University of Texas at Arlington is on record as being committed to both the spirit and letter of federal equal opportunity legislation; reference Public Law 92-112 - The Rehabilitation Act of 1973 as amended. With the passage of federal legislation entitled Americans with Disabilities Act (ADA), pursuant to section 504 of the Rehabilitation Act, there is renewed focus on providing this population with the same opportunities enjoyed by all citizens.

As a faculty member, I am required by law to provide "reasonable accommodations" to students with disabilities, so as not to discriminate on the basis of that disability. Student responsibility primarily rests with informing faculty of their need for accommodation and in providing authorized documentation through designated administrative channels. Information regarding specific diagnostic criteria and policies for obtaining academic accommodations can be found at www.uta.edu/disability. Also, you may visit the Office for Students with Disabilities in room 102 of University Hall or call them at (817) 272-3364.

Academic Integrity

It is the philosophy of The University of Texas at Arlington that academic dishonesty is a completely unacceptable mode of conduct and will not be tolerated in any form. All persons involved in academic dishonesty will be disciplined in accordance with University regulations and procedures. Discipline may include suspension or expulsion from the University.

"Scholastic dishonesty includes but is not limited to cheating, plagiarism, collusion, the submission for credit of any work or materials that are attributable in whole or in part to another person, taking an examination for another person, any act designed to give unfair advantage to a student or the attempt to commit such acts." (Regent's Rules and Regulations, Series 50101, Section 2.2)

Student Support Services

The University of Texas at Arlington supports a variety of student success programs to help you connect with the University and achieve academic success. These programs include learning assistance, developmental education, advising and mentoring, admission and transition, and federally funded programs. Students requiring assistance academically, personally, or socially should contact the Office of Student Success Programs at 817-272-6107 for more information and appropriate referrals.