112-FormalMethods1Overview of Formal Methods212-FormalMethodsTopics●Introduction and terminology●FM and Software Engineering●Applications of FM●Propositional and Predicate Logic●Program derivation●Intuitive program verification●Algebraic Specifications●Overview of Specification languages312-FormalMethodsTerminology●Methods:■general guidelines governing an activity■rigorous, systematic, and may be formal●Techniques:■are technical, mechanical, approaches■may have restricted applicability●Methodologies:combine methods. techniques●Tools: can be built to support methodology412-FormalMethodsComponents of a FormalMethod● Formal systems.■ formal languages with well-defined syntax■ well-defined semantics■ proof systems● Development technique.■ implementation produced from specification■ application of development steps■ refinement process● Verification technique.■ verify implementation satisfies specification■ verify each development step512-FormalMethodsFormal vs. Rigorous●Formal■based on mathematics (including logic)■validity of statements can be mechanically checked●Rigorous■ strictly follows the rules■ compliance can be audited612-FormalMethodsImportant characteristics of FM●Abstraction●Proof obligations●Tool support●Systematic process2712-FormalMethodsFM does not replace testing!●Reduces burden on testing phases to detect allcritical errors●Facilitates more effective allocation of testingresources●Can guide the selection of test cases812-FormalMethodsWhy Use Formal Methods●Improve quality of software system●Fitness for purpose●Maintainability●Ease of construction●Higher confidence in software product●Reveal ambiguity, incompleteness, and inconsistency insystem●Detect design flaws●Determine correctness912-FormalMethodsV&V and TraceabilityFormal SpecificationCodeThe Real WorldValidationVerification1012-FormalMethodsV&V and TraceabilityFormal SpecificationCodeThe Real WorldValidationVerificationTraceability1112-FormalMethodsTraditional verificationtechniques not successful. Why not?● Too much like math? (proofs, ugh!)● Notation too hard to use● Notation too hard to write out● "Simple" things take a lot of effort● "Complex" things seem impossible● Program verification is an undecidable problem● "If it works, why mess with it?"1212-FormalMethodsPotential solutions?:● Need experimental evidence on large projects.● Construction of support tools● Early education!?!?● Integration of formal methods in more than one phase ofsoftware engineering● Improved (automated) theorem proving strategies●Handle more than just functional properties●MOST IMPORTANTLY: do not verify "after the fact"31312-FormalMethodsWhen and Where?●Introduce FM into existing systems■Verify critical properties■Facilitate maintenance and reimplementation●Introduce FM into new systems■Capture requirements precisely■Reduce ambiguity■Guide software development process■Basis for testing■Formalize requirements analysis and design1412-FormalMethodsRushby’s “Levels of Rigor”●Level 0: No use of formal methods.■structured walk throughs, ‘formal’ inspections●Level 1: Use of concepts and notation from discrete mathematics.■cleanroom, SCR (software cost reduction)●Level 2: Use of formalized specification languages with somemechanized support tools.■specification languages, ‘rigorous’ proofs●Level 3: Use of fully formal specification languages withcomprehensive support environments, including mechanizedtheorem proving or proof checking.1512-FormalMethodsFormal Semantics●Formal semantics provide precise, machine-independentconcepts●Provide unambiguous specification techniques and arigorous theory to support reliable reasoning.●A formal definition of a language can suggest a method forconstructing programs guaranteed to conform to theirspecifications.●So, the purpose of formal specification is ...1612-FormalMethodsPurpose of FormalSpecification●The purpose of a formal specification is to statewhat a system should do without describing howto do it●A formal specification may define a system as anabstract datatype.●A formal specification should avoidimplementation bias.1712-FormalMethodsFormal Specifications●Formal specifications serve as a■contract■documentation■means of communication between client, specifier, andimplementer●Formal specifications are amenable to machineanalysis and manipulation1812-FormalMethodsToo Little and Too Much●There exists a balance between saying enoughin a specification and saying too much.■say enough so that implementers do not chooseunacceptable implementations■specifications should capture the requirementscompletely■avoid implementation-bias by not restricting freedomof later designers41912-FormalMethodsOperational Approach●Define an abstract machine having states, possibly severalcomponents, and some set of primitive instructions.●Define the machine by specifying how the components of the state arechanged by each instruction.●Define the semantics of a particular programming language in termsof states.●Abstract machines may be unrealistic from a practical point of view,but the simplistic definition prevents misunderstanding code later.2012-FormalMethodsOperational Approach con’t■The semantic description of the programming languagespecifies a translation into this code.■Trace through the translated program step-by-step todetermine its precise effect.■Languages defined in this way include PL/I (by theVDM method)2112-FormalMethodsThe Axiomatic Approach●Associate an "axiom" with each kind of statementin the programming language■state what may be asserted after execution of thatstatement in terms of what was true before■an example is the use of pre- and postconditions.2212-FormalMethodsAnother View●Model-Oriented: define system behavior by constructingmodel of system in terms of mathematical structures■tuples, functions. sets, or sequences■languages include VDM, Z, CSP, and Petri Nets●Property-Oriented: define system behavior indirectly bystating a set of properties that the system must satisfy2312-FormalMethodsTwo Types of Property-Oriented Approaches●Axiomatic: use first-order predicate logic (pre- andpostconditions)●Algebraic: use axioms in equational form todescribe