tailieunhanh - Lecture Formal methods in software engineering: What are formal methods?

After studying this chapter you will be able to understand: What are formal methods? Three levels of formal methods, use in the design process, weakness of natural language specifications, incomplete specifications, formal languages, advantages of formal methods, critical analysis, formal specification methods. | Formal Methods in Software Engineering Credit Hours: 3+0 By: Qaisar Javaid Assistant Professor Formal Methods in Software Engineering 1 What are Formal Methods? Formal Language Specification Formal Methods centred around a notation known as a formal specification language. Formal Semantics Mathematical base allows precise notions. Unambiguous. Allows consistency, correctness, specification and implementation to be expressed. Increase Human Understanding of Specified System. & Allow the possibility of formal reasoning and development. 2 Formal Methods in Software Engineering Three Levels of Formal Methods 1. Requirements Only 2. No Analysis/Proof 3. Cost effective 1. Produce a program in a more formal manner 2. Use proofs of properties or refinements from formal specification 3. Costly 1. Use theorem prover 2. Fully formal machine- checked proofs. 3. Expensive, hard and often costly 4. Formally prove the entire system. LEVEL 0 Formal Specification LEVEL 1 Formal Verification LEVEL 2 Theorem Provers 3 Formal Methods in Software Engineering Use in the Design Process Specification Description of system to be developed at any level of detail desired. Formal specification can be used: 1. to guide further development. 2. verify requirements of system are completely and accurately specified. 4 Formal Methods in Software Engineering Use in the Design Process Development Formal specification can be used as a guide to progress the development of the actual system. Model-Orientated Specification Observed behaviour of actual system compared to behaviour of specification. Property-Orientated Specification Preconditions and postconditions may be able to become assertions in executable code of system. 5 Formal Methods in Software Engineering Use in the Design Process Verification Formal specification can be used to prove certain properties of specification and hence the developed system. Human-Directed Proof Understand the system better Mathematical-style proofs . | Formal Methods in Software Engineering Credit Hours: 3+0 By: Qaisar Javaid Assistant Professor Formal Methods in Software Engineering 1 What are Formal Methods? Formal Language Specification Formal Methods centred around a notation known as a formal specification language. Formal Semantics Mathematical base allows precise notions. Unambiguous. Allows consistency, correctness, specification and implementation to be expressed. Increase Human Understanding of Specified System. & Allow the possibility of formal reasoning and development. 2 Formal Methods in Software Engineering Three Levels of Formal Methods 1. Requirements Only 2. No Analysis/Proof 3. Cost effective 1. Produce a program in a more formal manner 2. Use proofs of properties or refinements from formal specification 3. Costly 1. Use theorem prover 2. Fully formal machine- checked proofs. 3. Expensive, hard and often costly 4. Formally prove the entire system. LEVEL 0 Formal Specification LEVEL 1 Formal .