Introducing Formal Methods - MIT

1 1 Introducing Formal MethodsFormal Methods for Software specification and Analysis: An OverviewL 52 Software Engineering and Formal MethodsnEvery Software engineering methodology is based on a recommended development process proceeding through several phases: Analysis, specification ,Design,Coding,Uni t Testing, Integration and System Testing, MaintenancenFormal Methods can: Be a foundation for describing complex systems Be a foundation for reasoning about systems Provide support for program developmentnComplimentary approach to methodology!3 Testing: Static vsDynamic AnalysisnStatic analysis of code Does not require execution of code Lexical analysis of the program syntax and investigates and checks the structure and usage of individual statements; often automatednDynamic Analysis of code Involves running the system (testing) Program run formally under controlled conditions with specific results expected Path and Branch Testing4 What are Formal Methods ?

2 NTechniques and tools based on mathematics and Formal logicnCan assume various forms and levels of rigorOccasional mathematicalnotation embedded in EnglishspecificationsFully Formal specificationlanguages with a precisesemanticsspectrum of rigorleast rigorousmost rigorousL 55 Why Consider Formal Methods ?nSystems are increasingly dependent on software componentsnComplexity of systems with embedded software has increased rapidlynMaintaining reliability in software-intensive systems is very difficultSystemComplexityTimeL 56 Formal Methods ConceptsFormal specification MethodsFormalFormal ModelAbstractionSpecificationsProofsChec kingL 57 Formal SpecificationsnTranslation of a non-mathematical description (diagrams, tables, English text) into a Formal specification languagenConcise description of high-level behavior and properties of a systemnWell-defined language semantics support Formal deduction about specificationL 48 Types of Specifications InInformal Free form, natural language Ambiguity and lack of organization can lead to incompleteness, inconsistency, and misunderstandingsnFormatted Standardized Syntax Basic consistency and completeness checks Imprecise semantics implies other sources of error may still be present9 Types of Specifications IInFormal Syntax and semantics rigorously defined Precise form, perhaps mathematical Eliminate imprecision and ambiguity Provide basis for mathematically verifying equivalence between specification and implementation May be hard to read without training Semantic distance?

3 10 Formal SpecificationsnGoal: Describe external behaviour without describing or constraining implementationnFormal Method has 2 parts: Logical Theory: Means by which one reasons about specifications, properties and programs First order predicate calculus (quantification over variables) Second order predicate calculus (quantification over relations) Temporal logic Structuring Theory: Defines elements being reasoned about11 Types of Formal SpecificationsnProperty Oriented: State desired properties in a purely declarative way Algebraic: Data type viewed as an algebra, axioms state properties of data type s operations Axiomatic: Uses first order predicate logic, pre and post conditions Operational specification : Describe desired behaviour by providing model of systemnModel Oriented: Provide direct way of describing systembehaviour(sets, sequences,tuples, maps) : Abstract Model (in terms previously defined mathematical objects eg.)

4 Sets, sequences, functions, mappings) State machines12 Property Oriented: Algebraic SpecificationsnUses Input-Output Assertions Sets of operations Axioms specifying behaviour of operationsnTwo parts to a specification syntax axioms13 Model Oriented: Abstract Model SpecificationsnBuild an abstract model of required software behaviour using mathematically defined types (sets, relations)nDefine operations by showing effects of that operation on the modelnSpecification includes: Model Type Invariant properties of model For each operation Name, parameters, return values Pre-and Post-conditions14 Example Problem:The English SpecificationA space platform contains a number of instruments. Several communications channels are provided allowing both input and output instrument communications. Platform instruments may be placed in active or inactive states. Only active instruments may be assigned to I/O-channels. Active instruments may be assigned to more than one I/O-channel, up to some maximum number of I/O-channels per instrument.

5 Further, I/O-channels may be shared by several active instruments, up to some maximum number of instruments shared per objective is to construct a specification , that will manage the assignment of communication I/O-channels to spacecraft platform 515 Example AssignmentsABCDC1C2C3I/O ChannelsInstrumentsL 516Z specification :Basic Variables and InvariantsnInvariants are stated as the predicateIO_Channel_Assignments Basic_Typesactive_instruments : PPlatform_Instrumentsassigned_to : Communications_Channels Platform_Instrumentsavailable, busy: PCommunications_Channelsrange assigned_to [subset of] active_instrumentsavailable busy = L 517 CompletedMake_An_Assignment0 SchemaMake_An_Assignment0 IO_Channel_Assignments instrument? : Platform_Instrumentschannel? : Communications_Channelsinstrument? active_instrumentschannel? available#(assigned_to>{instrument?}) < Max_Channelschannel? -> instrument? assigned_toactive_instruments' = active_instrumentsassigned_to' = assigned_to {channel?}

6 ->instrument?}[#({channel?}<assigned_to) < Max_Instruments-1] \/[#({channel?}<assigned_to) = Max_Instruments-1/\available' = available -{channel?}/\busy' = busy {channel?}]L 518Z specification :Schema for Error ConditionInstrument_Not_Active IO_Channel_Assignmentsinstrument? : Platform_Instrumentsmessage! : Possible_Messageinstrument? active_instrumentsmessage! = instrument_not_activeL 519 Interesting Thought ProblemnAlice and Bill throw a party, and invite 4 other couples. As each couple arrived, there are greetings and handshakes. At the end of the party, Bill asked everyone, including Alice, how many people they shook hands with: Every answer was different! nHow many hands did Alice shake? : No one shakes hands with their own partner or themselves. You greet a person only Methods ConceptsFormal specification MethodsFormal Formal ModelAbstractionSpecificationsProofsChec kingL 521 Formal ProofsnComplete and convincing argument for validity of some property of the system descriptionnConstructed as a series of steps.

7 Each of which is justified from a small set of rulesnEliminates ambiguity and subjectivity inherent when drawing informal conclusionsnMay be manual but usually constructed with automated assistanceL 422 Model CheckingnOperational rather than analyticnState machine model of a system is expressed in a suitable languagenModel checker determines if the given finite state machine model satisfies requirements expressed as formulas in a given logicnBasic method is to explore all reachable paths in a computational tree derived from the state machine modelL 423 AbstractionnSimplify and ignore irrelevant detailsnFocus on and generalize important central properties and characteristicsnAvoid premature commitment to design and implementation choicesL 424 Program as Mathematical ObjectnProgram Mathematical ObjectnProgramming language Mathematical LanguagenCan prove properties about the programFIOF(I) O25 Formal specification LanguagesnBased on Formal mathematical logic, with some programming language enhancements (such as type systems and parameterization)nGenerally non-executable --designed to specify whatis to be computed, not how the computation is to accomplishednMost are based on axiomatic set theory or higher-order logicL 526 Features of specification LanguagesnExplicit semantics.

8 language must have a mathematically secure flexibility convenience economy of expressionnProgramming language data types records tuples 527 Features of specification Languages (cont d)nConvenient syntaxnDiagrammatic notationnStrong typing can be much richer than programming languages provides economy and clarity of expression type-checking provides consistency checksnTotal vs. partial functions most logics assume total functions subtypes can help make total functions more flexibleL 528 Features of specification Languages (cont d)nAxioms and definitions axioms can introduce inconsistencies and should be used judiciously definitional principle assures that definitions are well-formed in some languages ( PVS) type-checking conditions (to be proved) will be generated to assure sound definitionsnModularization breaking a specification into modules is an important organizational feature parameterized modules allow reusabilityL 529 Features of specification Languages (cont d)nBuilt-in model of computation to discharge simple type-checking constraints enhance proof-checkingnMaturity documentation tool support associated literature libraries of proven specifications some measure of standardizationL 530 Logical Errors in Formal SpecificationsL 5 Categories of Logical AnomaliesLikelyLogical inconsistency.

9 Easiest logical errors to the specification mean what is intended? System invariants can help in the specification identify all contingencies and specify appropriate behavior for all cases? Peer review can aid in for Detection of Errors in Formal SpecificationsnInspection of the Formal specification (manual)nParsing for syntactic correctness (automated)nType-checking for semantic consistency (automated)nSimulation/animation based on the specification (automated). Only possible if the language provides an execution proving, proof-checking, model-checking for logical anomaliesL 5 The following error detection techniques are listed in increasing order of rigor and cost of Specifications as a System DescriptionnClarify requirements and high-level designnArticulate implicit assumptionsnIdentify undocumented or unexpected assumptionsnExpose flawsnIdentify exceptionsnEvaluate test coverageL 533 Benefits of Formal SpecificationsnHigher level of rigor enables a better understanding of the problemnDefects are uncovered that would likely go unnoticed with traditional specification methodsnIdentify defects earlier in life cyclenCan guarantee the absence of certain defectsL 434 Benefits of Formal Specifications (cont d)

10 NFormal specification language semantics allow checks for self-consistency of a problem specificationnFormal specifications enable Formal proofs which can establish fundamental system properties and invariantsnRepeatable analysis means reasoning and conclusions can be checked by colleaguesL 435 Benefits of Formal Specifications (cont d)nEncourages an abstract view of system --focusing on whata proposed system should accomplish as opposed to howto accomplish itnAbstract Formal view helps separate specification from designnEnhances existing review processes by adding a degree of rigorL 436 Limitations to Formal MethodsnUsed as an adjunct to, not a replacement for, standard quality assurance methodsnFormal Methods are not a panacea, but can increase confidence in a product s reliability if applied with care and skillnVery useful for consistency checks, but can not assure completeness of a specificationL 537 Cautions in the Use of Formal MethodsnJudicious application to suitable project environments is critical if benefits are to exceed costsnFM and problem domain expertise must be fully integrated to achieve positive resultsL 538 ConclusionnFM are no panaceanFM can detect defects earlier in life cyclenFM can be applied at various levels of resource investmentnFM can be integrated within existing project process modelsnFM can improve quality assurance when applied judiciously to appropriate projectsL 5