Lecture Formal methods in software engineering: Software verification using formal methods. In this chapter, the following content will be discussed: Formal methods in block handler, data invariant, block handler, block handler, selection criteria, formal clean room software engineering,. | Formal Methods in SE Software Verification Using Formal Methods By: Qaisar Javaid, Assistant Professor Formal Methods Formal Methods Formal Methods in Block Handler Concept Current methods of software development involves only combination of diagrams, text, tables etc. No methods are used to test the correctness of the end result in each of stages of software development for . requirement specification, design etc. This may lead to contradictions, ambiguities, incompleteness, vagueness etc. This may not be a good option for safety-critical or mission critical systems,where failure may have high price Concept Formal methods allow a software engineer to create a specification that is more consistent and unambiguous Set theory and logic notations are used to create a clear statement of facts (requirements) which can then be analyzed to prove correctness and consistency Since specification is created using mathematical notation, it is inherently less ambiguous than informal modes of representation. Definitions Data Invariant A data invariant is a condition that is true throughout the execution of the system that contains a collection of data. . maximum number elements in any system, duplication not allowed in a system. State A state is the stored data that a system accesses and alter. Definitions Operation It is defined as action that takes place in a system and reads or writes data to a state It is associated with 2 conditions Precondition Postcondition Precondition defines whether the operation is valid or not and Postcondition defines what happens when an operation has completed its action Example Block Handler A common part of any operating system which handles the memory blocks Provides free blocks of memory to new created files and regains blocks when file is removed. It keeps tracks of free blocks or the unused blocks and the used blocks Whenever a block is freed, it is added to the queue of unused blocks and similarly whenever a block is needed . | Formal Methods in SE Software Verification Using Formal Methods By: Qaisar Javaid, Assistant Professor Formal Methods Formal Methods Formal Methods in Block Handler Concept Current methods of software development involves only combination of diagrams, text, tables etc. No methods are used to test the correctness of the end result in each of stages of software development for . requirement specification, design etc. This may lead to contradictions, ambiguities, incompleteness, vagueness etc. This may not be a good option for safety-critical or mission critical systems,where failure may have high price Concept Formal methods allow a software engineer to create a specification that is more consistent and unambiguous Set theory and logic notations are used to create a clear statement of facts (requirements) which can then be analyzed to prove correctness and consistency Since specification is created using mathematical notation, it is inherently less ambiguous than informal .
