F8

Question 1

How to detect errors?

Answer 1

• Testing
+ Direct on the product, immediate relevance, quick
– Diagnosis needs complete observability
– Errors detected late are costly
• Simulation
+ Can be performed through the design stage
– Simulato rcan be significantly slower than real system
- Exhaustive testing and simulation is nearly impossible

Question 2

What is Formal Methods

Answer 2

Formal methods is that area of computer science that is concerned with the application of mathematical techniques to the design and implementation of computer hardware and software.

Question 3

two main parts to formal methods:

Answer 3

– Formal specification: Using mathematics to specify the desired properties of a computer system.
– Formal verification: Using mathematics to prove that a computer system satisfies its specification.

Question 4

Advantages of Formal Methods

Answer 4

• Higher level of rigor enables a better understanding of the problem
• Identify defects earlier in life cycle
• Can guarantee the absence of certain defects
• Logically consistent way of reasoning
• Exhaustive coverage, often impossible to achieve by others
• Mechanization and automation => correctness
• Summary: It can help to understand the problem/system and have much stronger guarantee than other methods.

Question 5

Disadvantage of Formal Methods

Answer 5

• Push-button methods (model checking) has limited applicability (usually states explosion)
• More powerful methods (theorem proving) require mathematical skills (and very difficult for larger system)
• Theoretical limitations: decidability, complexity, halting problem, incompleteness
• In practice: speed, simplicity, robustness, money…
• Summary: It has its limitations to guarantee anything (no absolute guarantees) while at the same time it is extremely costly.