author: aman

Blog II - Part I - Day 08

The last blog was written by Kaushik, the Applied Physics Freshman student, beautifully covered the diverse applications of Blockchain and the challenges/risks involved with the use of the current form of Blockchain technology.

This blog will cover straight definitions and their super intuitive explanations(as far as I can make), about the FORMAL METHODS & VERIFICATIONS. What are they? and Why are they?

Plus I’ll try to give a brief about my work, in the later part of this blog.(in another micro-blog)

Buckle up a bit, the logics and thinking coming up…

In this micro-blog

  • Formal Methods
  • Formal Verification
  • First Order Logic
  • ….. will keep adding
—–

There was a series of events which motivated me to begin this series.

This was when I was talking to one of the Sophomore year members in CEV, Shtakshi, Comps. Shtakshi has a huge interest in mathematics and love logics, but as a normal sophomore problems, she has a lot of options to explore because of which she didn’t have any particular choice.

As a normal 3rd year member’s job suggests, I tried explaining her about the field I have worked on, The FORMAL METHODS, and how crucial is it for Computer Researches.

I will put up a more “formal” definition and a more “informal” definition. You can always miss the formal definitions.

Formal Language:

Formal Definition says: (You can skip though)

In mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consist of symbols, letters, or tokens that concatenate into strings of the language.[1]

Informal Definition says:

It is just like, when you use normal languages(say english), what you brain really comprehends is only what that sentence “actually” means, and not the meaning of each word (eg. “the boy is running” your brain comprehends it to the “boy” & “running”) or You say “I have Ice-cream rolls, the roll, x, such that 1cm3 < x < 5cm3, goes to box A, <1cm3 goes to B, and >5cm3 goes to C….. What brain really comprehends here is 3 boxes, 3 categories, and place the ICE-CREAM rolls accordingly.”

The first formal language is thought to be the one used by Gottlob Frege in his Begriffsschrift (1879), literally meaning “concept writing”, and which Frege described as a “formal language of pure thought.”

This is the formal languages are all about. You just have to write what actually exists and is important. Just in case you need actual example[2]

Formal Methods:

Formal Definition says: (You can skip this one too) Find wikipedia definition here[3]

Informal Definition says: Whenever you try to use these formal languages to represent “states” (or say various computer states), and derive a few specifications of the computer systems, then the representation is called as the Formal representation and the deriving specifications and using them is called Formal Methods.

States are the condition in which a system currently is. For e.g. "”A light switch can be either on or off, and it can be toggled from one or the other. The current position of the switch (on or off) is the state of the switch. If you change the position of the switch you have changed it’s state.

Specifications are simply a few states that a system “must follow” and a few that a system “must not follow”.

If you wonder this thing can be applied to literally anything. Computer Sciences are just an application.

For e.g. “A machine in a factory has a lever, a grinder and a conveyer belt” So, you may “always want” a state when the following happen -> Lever is lifted up (i.e. the machine is on) -> Conveyer belt is running -> Grinder is running

could be represented as follows:

Unfaulty state

| Part | (1-> on, 0-> off) | | ———– | ———– | | Lever | 1 | | Conveyer Belt | 1 | | Grinder | 1 |

but, you may never want a state where the lever is ““off”” but the conveyer belt is running. i.e.

faulty state

| Part | (1-> on, 0-> off) | | ———– | ———– | | Lever | 0 | | Conveyer Belt | 1 | | Grinder | 1 |

imilarly, this works for every computer system. And thus, used largely in Computer Science Researches, specially when researching for bugs and vulnerabilities in the system.

Formal Verifications:

When you use, these methods to “Verify that the system under observations is following certain specfications or not”, these methods are called the Formal Verifications.

Hope that gets clear.

Please share the blog to make its reach high.

Thank you for your time. Gears down!!!