This course is very interesting for me because of two reasons:
1. I unwittingly studied a formal method.
2. I smoothly got introduced to automata theory.

Back when I was working on my undergraduate thesis, some of my friends who worked together in the ATN TP4/CLNP Networking Suite project got a topic to apply formal methods to different parts of the networking suite. At that time, I knew nothing about formal methods. Since my university is focusing on the practical side of computer science, we didn't have courses on things like automata and formal methods. So, my friends were planned to follow a short course in formal methods at another university. However, from the first meeting with the professor at the other university, it was concluded that my friends wouldn't be able learn formal methods in time to complete their theses because they lacked prerequisite subjects like automata theory. Therefore, formal methods remained a mystery for me.

In my first semester at RWTH Aachen, there was a really nice course titled "Formal Methods for Embedded Systems". Unfortunately, it was taught in German. So, formal methods remained a mystery for me still. But, throughout the semester, I heard that Model Checking is an important method to do verification of embedded systems. Since I want to specialize in embedded systems, I took this course in the second semester. A very brief statement about formal methods was given in the lecture and in the book: formal methods are the application of mathematics for modeling and analyzing ICT (Information & Communication Technology) systems. So brief it was that it didn't enter my mind that model checking is one of such methods. So, I was surprised when I discovered during the exam preparation that actually I had been studying a formal method for one semester.

Reflecting on the experience during my undergraduate study and what I have learned from this course, actually my friends should have been able to apply model checking as a formal method to check parts of the networking suite since they only needed to model the software using a modeling language like Promela and formulate properties that they want to check in either LTL or CTL formula before giving those two things to a model checker like NuSMV. All without the need to study automata theory since they were only going to use a model checker not to develop one. I think a crash course on developing a model and the properties by employing examples running on NuSMV should take at most one month. It would even be faster if the examples are taken from the parts of the networking suite that will be model checked.

So, coupled with the preview of "Formal Methods for Embedded Systems" that were given in the "Introduction to Embedded Systems" course, now I understand what formal methods are.

That is for the first reason. Now on to the second reason. In my first semester at RWTH Aachen, I tried to follow two theoretical courses that I didn't have back in my undergraduate study: Infinite Computations and Regular and Context-Free Languages. But, it turned out that the courses were too advanced for me since familiarity with automata theory was required. In this course, however, although automata theory is a prerequisite, the focus is not on the automaton itself, which is the case in the two aforementioned theoretical courses, but on the usage of automata. So, I could quickly learn about automata from the given definition and the numerous usage examples as well as the application of pumping lemma to solve one of the assignments. Of course, I still need to learn automata theory to get to know other interesting properties. But, this course has helped me to get some clues as to what I should expect when learning automata theory.

That is for the second reason. Now on to some stuff about the course itself. The trickiest things that I found throughout the semester are as follows:
1. Differentiating safety property and liveness property. Finally I came to understand those properties and put some notes on them in the last pages of my lecture notes.
2. Understanding an informally stated linear-time property and constructing the corresponding regular language. This can be seen in the assignments and the corresponding solutions.

Interesting trick that I found from the class is the table trick to find all elementary sets of the closure of an LTL formula in order to algorithmically construct the GNBA of the LTL formula. I also learned to always think about the negation of a logic formula after I made a mistake in applying the transition rules of the GNBA (e.g., when reading "a U b in B <-> b in B V (a in B /\ O(a U b) in B')", I should also read it as "a U b notin B <-> b notin B /\ (a notin B V O(a U b) notin B')").

To conclude, this course is highly recommended for those studying Informatics or Computer Science or Software Engineering since it is both theoretically interesting and practically useful. Also, it is very possible to study directly by understanding the textbook and doing some of the assignments whose solutions can be found in my lecture notes.

I highly recommend the textbook that is titled Principles of Model Checking by Christel Baier and Joost-Pieter Katoen who is the professor that teaches this course because the textbook makes the topic very accessible.

My lecture notes can be found at https://docs.google.com/leaf?id=0B8Lv3_mLLEBcYzBhMTZhOWMtY2MxNy00Y2Y1LWI... while the materials can be found at https://docs.google.com/leaf?id=0B66kEP2FWgm_MGVkY2Q4ZDUtZDA1Zi00Y2EwLWJ...