In this chapter, the following content will be discussed: Software reliability, what are formal methods? typical situation, some concerns, some exaggerations, the unbearable easiness of grading, different types of software, verification methods,. | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture 05 2 Some related books: Also: Mainly: 3 Goal: software reliability Use software engineering methodologies to develop the code. Use formal methods during code development 3 2 4 What are formal methods? Techniques for analyzing systems, based on some mathematics. This does not mean that the user must be a mathematician. Some of the work is done in an informal way, due to complexity. 4 5 Examples for FM Deductive verification: Using some logical formalism, prove formally that the software satisfies its specification. Model checking: Use some software to automatically check that the software satisfies its specification. Testing: Check executions of the software according to some coverage scheme. 5 6 Typical situation: Boss: Mark, I want that the new internet marketing software will be flawless. OK? Mark: Hmmm. Well, ., Aham, Oh! Ah??? Where do I start? Bob: I have just the solution for you. It would solve everything. 6 7 Some concerns Which technique? Which tool? Which experts? What limitations? What methodology? At which points? How expensive? How many people? Needed expertise. Kind of training. Size limitations. Exhaustiveness. Reliability. Expressiveness. Support. 7 8 Badmouth Formal methods can only be used by mathematicians. The verification process is itself prone to errors, so why bother? Using formal methods will slow down the project. 8 9 Some answers. Formal methods can only be used by mathematicians. Wrong. They are based on some math but the user should not care. The verification process is itself prone to errors, so why bother? We opt to reduce the errors, not eliminate them. Using formal methods will slow down the project. Maybe it will speed it up, once errors are found earlier. 9 10 Some exaggerations Automatic verification can always find errors. Deductive verification can show that the software is completely safe. Testing is the only industrial practical method. 10 11 Our approach . | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture 05 2 Some related books: Also: Mainly: 3 Goal: software reliability Use software engineering methodologies to develop the code. Use formal methods during code development 3 2 4 What are formal methods? Techniques for analyzing systems, based on some mathematics. This does not mean that the user must be a mathematician. Some of the work is done in an informal way, due to complexity. 4 5 Examples for FM Deductive verification: Using some logical formalism, prove formally that the software satisfies its specification. Model checking: Use some software to automatically check that the software satisfies its specification. Testing: Check executions of the software according to some coverage scheme. 5 6 Typical situation: Boss: Mark, I want that the new internet marketing software will be flawless. OK? Mark: Hmmm. Well, ., Aham, Oh! Ah??? Where do I start? Bob: I have just the solution for you. It would solve everything. 6 7
