MSE | CMU | SUBJECT
What are Formal Methods |Guide to CMU: 17–614
A brief introduction to Formal Methods from a Student
If you would have asked me what are formal methods before I came to CMU I would have thought it was a other long lost language which was used in old age computer systems to establish a sense of rules of regulations of using hardware for software computation.
And now that I have qualified the class of Formal Methods this is a intro guide on what to expect on the course. The following article only covers the course content and does not delve into other parts like quiz , assignments and teaching in general in great detail.
NOTE**: None of the below images , examples or visuals are from the official course but from the internet or other sources. The below things do not represent official course content but only concepts.
What is Formal Methods ?
So remember the Mr Beast YouTube video where the participant has to destroy $500,000 any way possible and Mr Beast tries to destroy his setup with tanks.
Consider Formal Methods as something similar except you are the tanks.
In simple terms formal methods makes use of models and logics for analysing the properties of a system and characterizing them and finding gaps.
You build a castle with all the money and you use a software which uses the concepts of Formal Methods to find gaps in you castle , the characteristic and rules your castle follows and makes sure it follows all the requirements.
As per Wikipedia
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems.
Do we need Formal Methods
The use of Formal methods is for defining properties of large scale software systems and ensuring that it aligns to a set of requirements and performs efficiently to different use cases.
How useful is it ? Not sure since as a student this is the first time I am encountering it and the class did not have enough examples of its usage however it is heavily used in companies like Amazon and Boeing but falls under a very particular niche.
I am going to note down some of the things you can expect from this course.
The start of the Beginning
Up to assignment 4 the goal is to get you into the basics of Formal Methods , the stuff is lot theoretical and builds a foundation towards the future stuff.
There are a bunch of stuff which gets introduced and I am giving a very small peek into the high level details.
State Machines: A mathematical model used to describe the behaviour of a system through a finite number of states and transitions between them.
Majority of the course is concerned about how can we define the logic and properties of state machines and what are the states that we should know about.
The above example demonstrates a bunch of state machines and their behaviour when one of them occurs.
Formal System: An abstract framework used to define and study logical reasoning through a structured set of rules, symbols, and axioms.
Propositional Logic: deals with propositions, which are statements that are either true or false.
The course requires you to prove such statements in detail using a set of rules and regulations explained deeper in the course.
I found that the course started picking its complexity from this point onwards and the rest of the course depended on our understanding of these concepts.
An example of that is this
Don't worry if you don't understand all these terms it just represents what you will be doing during the course.
Predicates: Functions that describe properties or relationships (e.g., “x is a human”).
Predicate Logic: extends propositional logic by introducing predicates and quantifiers
A lot of the course crosses around these lines and a lot of learning is about propositional and predicate logic. An example of this is like this.
I found proofs for these tricky as they consist of many rules and you have to balance between taking assumptions and following the rules. At most that we as students had to deal with were 2 nested assumptions for proofs.
The course assignments are done in latex and a huge emphasis is put into proper formatting and structure and these are the areas where it can get complex as you need to end assumptions and put proper table formatting in the right order.
The rest of the course depends on the understanding of predicate logic and the questions become more complex and require harder proofs compared to the one shown above.
You will be required to translate sentences to predicate logic , derive proofs and define set of predicates to translate a system.
Set Comprehension: a concise way of defining sets by specifying the properties that its elements must satisfy.
Set comprehension is the easiest part of the course so much that they dont even bother asking this in the finals and is only given in one assignment , so make sure to complete that well and get good points.
Starting with the Complex Stuff
The second half of the course as I like to call it builds on the previous concepts of the course and comes to reasoning of state machines as a way to mix all the things learnt.
This is one area you have to practice much more and concludes with a big concept — Describing the functionality with a set of states.
This is a concept that is beyond the scope of the blog but uses all the previous concepts to build real systems.
Describing functionalities is what I felt was close to setting requirements and unlike the other concepts of the course which have a defined answer these are different as it depends on the individual defining their structure.
As a student you are given a set of requirements of a system and you must build state machines and define their behaviour to align with the requirements.
ALLOY
This is the part where you start building your tanks to verify your software and its properties.
Alloy is a declarative specification language and analysis tool used in software engineering to model and analyse the structure and behaviour of systems. It is based on relational logic, which combines first-order logic with set theory and relational algebra.
This is the software we use for exploring the software designs , identifying issues and verifying the properties of the system.
A good example is the one below , you are defining the software for a course enrolment system with students and teachers and define your system in this manner.
// Define a base signature for Person
abstract sig Person {}
// Define Student and Teacher as subsets of Person
sig Student extends Person {}
sig Teacher extends Person {}
// Define a Course signature
sig Course {}
// Relationships: Students enroll in courses, Teachers teach courses
sig Enrollment {
student: one Person,
course: one Course
}
sig Teaching {
teacher: one Person,
course: one Course
}
// Run command to generate instances
run {} for 3 but 2 CourseWhen you run this code through alloy , alloy generates bunch of different simulations where you have a chance to identify potential issues.
The above code is not very complex however you will see an issue that a student can enrol in a class and even teach that class. We are missing a constraint that explicitly states that a student cannot be a teacher for a course they are enrolled in.
The second part covers Alloy in a major portion , developing software for different use cases.
This also comes up in the final exam and I would recommend you learn this well because there is a huge difference in writing alloy code in the software vs writing it in pen and paper for the exam. Train yourself enough that you can cover concepts of alloy well enough to not depend on the software.
FSP
It is a formal specification language used to describe and analyse concurrent systems based on finite state machines. It is particularly useful for modelling the behaviour of systems that involve multiple interacting processes.
The next part of the course follows on this to define systems and understand the relations between them.
An example code of this is like this
// Define the behavior of a traffic light
TRAFFIC_LIGHT = RED,
RED = (green -> GREEN),
GREEN = (yellow -> YELLOW),
YELLOW = (red -> RED).
// Run the system
||SYSTEM = (TRAFFIC_LIGHT).This shows the system out to be like this
You have to define such systems and show their interaction between them.
I would say this is one of the easier parts of the course and you can master it easily. For the final exam this is the scoring portion as the questions are straightforward but make sure to focus on formatting and understanding the question.
Practical Uses of Formal Methods
- Amazon uses TLA+ to design services: This shows how Amazon uses TLA+ , concepts of Formal methods to design large scale distributed systems. It covers services like DynamoDB and S3 and how Amazon engineers found out corner cases to anticipate. [Paper Link]
- Correctness of the Chord Protocol: Formal Methods was used to reveal critical flaws in the Chord protocols original design.
- Eclipse based IDE Verification: An Eclipse-based IDE was developed to simplify the design, verification, and implementation of security protocols using formal methods.
- Protocol Design using Alloy: A leader election protocol for distributed systems was modelled and analysed using Alloy.
General Advice
If I were to advise myself once again before taking this course this is what I would give myself.
- Practice questions: A lot of the concepts like proofs , alloy and translations are not easily understandable. Make sure to practice questions from back of the textbook or do the assignments well enough.
- Assignments: These form the bulk of your coursework and always double check before you submit them. A single formatting error or a missing bracket is enough to take out marks and you really don't want to do that for assignments.
- Quizzes: Quizzes are held every week and make sure you study and give them, you will be given ample time to answer the questions so make sure you study the current week and previous week concepts. Errors in quizzes can make or break you grade remember that.
- AI tools: Using AI tools is allowed in the assignments as long as you mention it. So use AI to learn concepts but remember if you use AI and don't mention it you can get marks cut off.
- Final Exam: Study together for this exam with your friends , you get to bring a 10 page cheat sheet. Solve previous years papers with your group to learn faster and make sure to reach early for the exam. This year our exam was held at 8AM so wake up early and leave.
- Cheat Sheet: Always aim to build your own cheat sheet or if you are studying in a group make a common cheat sheet but be aware which concepts are in which page. You can hit two birds with one stone , build your cheat sheet and also study.
- Participation credit: participate in office hours and attendance for participation marks and make sure to verify them from the instructor at the end of the mini on how much you actually got compared to what you were expecting.
- Textbook source of truth: All your assignment answers must follow the textbook. Even after getting your approach verified from TA’s double check them.
Conclusion and Final Thoughts
This is the entire Formal Methods course. The full extent of the course cannot be covered in a single blog but the general thing looks like this. The concepts and practice for the topics goes much much more than what is covered here but starts with these things.
As I mentioned before I feel this is a particular niche topic and as a student I am not sure I can foresee its use right now maybe somewhere in the future. However what this covers is a very small portion of formal methods and to actually do the proper stuff like mentioned in the practical use cases of formal methods it is taught in 17–624 Advanced Formal methods.
Our year advanced formal methods was not provided for mini-2 and so we are in a situation like the anime Death Note where the user can neither go to heaven or hell , we are in a place where we know Formal methods enough to have a conversation or mention it during our interviews but not enough to actually use it practically.
Furthermore for Mini 1 this is one of the core technical subjects offered and if you a non professional the other one would be Design patterns so how good that decision is depends on each person. Some people preferred something more technical , some people enjoyed formal methods as a good addition to their skillsets.
How you feel will depend once you start with the course , if you find the above concepts confusing read it once again mid way through the semester and once you end it.
If you would like more regular updates about coursework please checkout my other blogs where I have covered them.
If you found this blog useful consider subscribing and liking for it get engagement.
Study hard until then.
