605.729.8VL - Formal Methods

Course Structure

This course flow is based on (1.) coverage of main formal methods concepts, (2.) research on formal methods, (3.) discussion on formal methods concepts, (4.) application of formal methods to a problem/solution.

The course materials are divided into modules, (fall and spring) one for each week of the course, and (summer) two for each week of the course. While lectures will occur in a physical/virtual classroom each week, all course materials and assignments will be housed in Blackboard and Microsoft Teams. The module content can be accessed by clicking Course Modules on the left menu. A module will have several sections including the overview, content, readings, discussions, and assignments. You are encouraged to preview all sections of the module before starting. Most modules run for a period of seven (7) days, exceptions are noted in the Course Outline. You should regularly check the Calendar and Announcements for assignment due dates.

Course Topics

• Introduction to Formal Methods
• Set-theoretic Specifications
• Prolog, Coq Framework
• Elements of Z (Structure, Logic, Synthesis)
• Formal Reasoning in Z
• Application Examples in Z
• Temporal Logic
• Specification in Temporal Logic
• Deduction in Temporal Logic
• Model Checking
• Applications of Temporal Logic
• Grammars
• Automated Proofs, Theorem Proving

Course Goals

This course is an introduction to this vast world of formal methods. We will focus on the formal verification of the widest possible variety of programming language features and techniques. Each student will carry out an investigation of one or another of the existing formal verification systems, applying it to a system or program of the student’s choice.

Course Learning Outcomes (CLOs)

• Introduce fundamental structures and tools in mathematics and computer science used for formal methods.
• Differentiate formal specification, formal verification and formal machine-checked theorem provers.
• Apply formal mathematical methods for elementary computation problems and their solutions.
• Develop skills for analyzing computational problems and implementing formal methods to specify and verify solutions.
• Survey and research application areas and apply heuristics to analyze and understand specific formal method approaches.

Textbooks

Textbook information for this course is available online through the appropriate bookstore website: For online courses, search the MBS website.

Required

Most of the required material and content will be presented through Jupyter notebooks.

Optional

Jacky, Jonathan. The way of Z: practical programming with formal methods. Cambridge University Press, 1997. ISBN-13: 978-0521559768

Fisher, Michael. An introduction to practical formal methods using temporal logic. Vol. 82. Hoboken: Wiley, 2011. ISBN-13: 978-0470027882

Required Software

Microsoft Teams

This course will use Microsoft Teams for our Discussions and general communication. This is a platform that works in your browser, on your desktop, and has an app for tablets and phones (iOS and Android). This will allow you to participate in the Discussions and ask questions from whatever device you are most comfortable.

To access Teams, click the Microsoft Teams link on the course menu in Blackboard. You can also download the desktop or mobile app. Sign in with your JHU email using @jh.edu (NOT @jhu.edu) and JHU password. You should see our Team listed on the left-hand side with the Team channels (discussion areas) listed below.

There are various channels for discussion, including a General channel that is for discussion general topics and questions related to the course assignments and content. Use your assigned Discussion Group channels for answering Discussion posts—you will be assigned to a different Discussion Group for each Discussion in the course. Be sure to manage your notification settings so you know when there are new posts. It’s highly recommended that you be sure to subscribe to the General channel.

For more information, check out the instructions for getting started with Microsoft Teams. If you have difficulty logging in or accessing Microsoft Teams, please contact the Help Desk at ep-help-desk@jhu.edu.

Jupyter Notebook

This course will use Python as its programming language, which is deemed as the number 1 data science programming language (reference: online resources). This course will also use Jupyter Notebook, which is a document that contains both code and rich text elements, such as figures, links, and Latex equations. A Jupyter notebook about the Jupyter Notebook itself is provided in the first module. This notebook contains how to install the Anaconda Python development environment that will be used in this course.

Student Coursework Requirements

It is expected that each module will take approximately 10–16 hours per week to complete. Here is an approximate breakdown:

• Attending physical or Virtual Live classroom sessions (3 hours per week)
• Reading the assigned sections of the texts (approximately 1–2 hours per week) as well as some outside reading
• Completing assignments (approximately 4–8 hours per week)
• Researching the paper topic and engaging in weekly discussions (approximately 2–3 hours per week)

This course will consist of the following basic student requirements:

Class Participation (10% of Final Grade Calculation)

You are responsible for carefully reading all assigned material and being prepared for both the Virtual Live classroom sessions and Discussions. The majority of readings are from the course text. You will be responsible for all assigned reading material, whether we cover it in class or not, so prepare questions about parts of the readings not understood. There may also be optional readings recommended from the archival literature.

Discussions (20% of Final Grade Calculation)

About 3 over the semester, will run for about 3 weeks each – student generated – students post research/resources for discussion – reports will be produced by student teams.

Assignments (40% of Final Grade Calculation)

Assignments will include real-world problems. Although the Assignments will usually reflect the current material, I will also give on occasion a brain-building problem that may no direct relation to the material but rather may require basic logical reasoning to solve.

Assignments are assigned more-or-less every week and can involve basic materials, further examination of concepts introduced and presented in class and in the textbook, brainteasers, and more challenging questions problems. Problems will be the basis for class discussions as well; be prepared to ask and answer questions and discuss the problems.

Any course materials prepared for evaluation for grades must be turned in Canvas in PDF format. All assignments are due according to the dates in the Calendar. If there is a legitimate reason why an assignment is going to be late and this can be known in advance (i.e., excluding illness) then the instructor must be notified of such. Illness is a legitimate excuse for lateness but please let me know as soon as possible and we can make arrangements for delivery. NO ASSIGNMENTS WILL BE ACCEPTED IF SUCH NOTIFICATION WAS NOT MADE.

Refer to the Assignment Guidelines for more information.

Research Paper (30% of Final Grade Calculation)

The research project paper will involve the theoretical and experimental analysis of a problem/solution using formal methods. I will provide a list of applications to be selected from (not exclusively, as students may bring their own). Students are expected to develop a project, which has the introduction to the problem/solution/program, the mathematical analysis, specification, verification, experimental setup, scenarios, and conclusions. The script may be acquired from other sources provided that references are given and the script is "made your own". i.e. similar to writing a research paper. Please check the course Project Rubric.The project will be accepted in a Jupyter notebook format or in a publication quality manuscript. More details about the project and expectations are provided in the Project Rubric.

Grading Policy

Assignments are due according to the dates posted in your Blackboard course site. You may check these due dates in the Course Calendar, Course Outline, or the Assignments in the corresponding modules. I will post grades one week after assignment due dates.

We generally do not directly grade spelling and grammar. However, egregious violations of the rules of the English language will be noted without comment. Consistently poor performance in either spelling or grammar is taken as an indication of poor written communication ability that may detract from your grade.

A grade of A indicates achievement of consistent excellence and distinction throughout the course—that is, conspicuous excellence in all aspects of assignments and discussion in every week.

A grade of B indicates work that meets all course requirements on a level appropriate for graduate academic work. These criteria apply to both undergraduates and graduate students taking the course.

EP uses a +/- grading system (see “Grading System”, Graduate Programs catalog, p. 10).

Score Range	Letter Grade
100-98	= A+
97-94	= A
93-90	= A−
89-87	= B+
86-83	= B
82-80	= B−
79-77	= C+
76-73	= C
72-70	= C−
69-67	= D+
66-63	= D
<63	= F

Final grades will be determined by the following weighting:

Item	% of Grade
Class Participation	10%
Discussions	30%
Class Project	60%

Academic Policies

Deadlines for Adding, Dropping and Withdrawing from Courses

Students may add a course up to one week after the start of the term for that particular course. Students may drop courses according to the drop deadlines outlined in the EP academic calendar (https://ep.jhu.edu/student-services/academic-calendar/). Between the 6th week of the class and prior to the final withdrawal deadline, a student may withdraw from a course with a W on their academic record. A record of the course will remain on the academic record with a W appearing in the grade column to indicate that the student registered and withdrew from the course.

Academic Misconduct Policy

All students are required to read, know, and comply with the Johns Hopkins University Krieger School of Arts and Sciences (KSAS) / Whiting School of Engineering (WSE) Procedures for Handling Allegations of Misconduct by Full-Time and Part-Time Graduate Students.

This policy prohibits academic misconduct, including but not limited to the following: cheating or facilitating cheating; plagiarism; reuse of assignments; unauthorized collaboration; alteration of graded assignments; and unfair competition. Course materials (old assignments, texts, or examinations, etc.) should not be shared unless authorized by the course instructor. Any questions related to this policy should be directed to EP’s academic integrity officer at ep-academic-integrity@jhu.edu.

Students with Disabilities - Accommodations and Accessibility

Johns Hopkins University values diversity and inclusion. We are committed to providing welcoming, equitable, and accessible educational experiences for all students. Students with disabilities (including those with psychological conditions, medical conditions and temporary disabilities) can request accommodations for this course by providing an Accommodation Letter issued by Student Disability Services (SDS). Please request accommodations for this course as early as possible to provide time for effective communication and arrangements.

For further information or to start the process of requesting accommodations, please contact Student Disability Services at Engineering for Professionals, ep-disability-svcs@jhu.edu.

Student Conduct Code

The fundamental purpose of the JHU regulation of student conduct is to promote and to protect the health, safety, welfare, property, and rights of all members of the University community as well as to promote the orderly operation of the University and to safeguard its property and facilities. As members of the University community, students accept certain responsibilities which support the educational mission and create an environment in which all students are afforded the same opportunity to succeed academically. 

For a full description of the code please visit the following website: https://studentaffairs.jhu.edu/policies-guidelines/student-code/

Classroom Climate

JHU is committed to creating a classroom environment that values the diversity of experiences and perspectives that all students bring. Everyone has the right to be treated with dignity and respect. Fostering an inclusive climate is important. Research and experience show that students who interact with peers who are different from themselves learn new things and experience tangible educational outcomes. At no time in this learning process should someone be singled out or treated unequally on the basis of any seen or unseen part of their identity. 
 
If you have concerns in this course about harassment, discrimination, or any unequal treatment, or if you seek accommodations or resources, please reach out to the course instructor directly. Reporting will never impact your course grade. You may also share concerns with your program chair, the Assistant Dean for Diversity and Inclusion, or the Office of Institutional Equity. In handling reports, people will protect your privacy as much as possible, but faculty and staff are required to officially report information for some cases (e.g. sexual harassment).

Course Auditing

When a student enrolls in an EP course with “audit” status, the student must reach an understanding with the instructor as to what is required to earn the “audit.” If the student does not meet those expectations, the instructor must notify the EP Registration Team [EP-Registration@exchange.johnshopkins.edu] in order for the student to be retroactively dropped or withdrawn from the course (depending on when the "audit" was requested and in accordance with EP registration deadlines). All lecture content will remain accessible to auditing students, but access to all other course material is left to the discretion of the instructor.