Formal Methods I - Rose-Hulman Institute of Technology

Formal Methods I - Rose-Hulman Institute of Technology

Formal Methods: Z CS 415, Software Engineering II Mark Ardis, Rose-Hulman Institute March 18, 2003 Outline Types of Formal Methods Introduction to Z Examples 2

Formal Methods Specification and verification methods Have formal (mathematical) semantics unambiguous facilitate proofs of correctness

In use since late 1970s more popular in Europe than US still only a niche market 3 Types of Formal Methods Model-theoretic

VDM, Algebraic ACT One, Larch , OBJ Concurrent processes

CCS, Z CSP, Petri Nets Finite State Machines Esterel,

Statecharts Hybrid LOTOS, SDL 4 Model-theoretic Methods

Vienna Development Method (VDM) invented at IBM Vienna lab in late 1970s used for compilers (Denmark, Germany) and for information processing (England) Z Invented

by Jean-Raymond Abrial (France) Developed by Programming Research Group (PRG) at Oxford Used at IBM Hursley in mid 1980s 5 Foundations of Z Model theoretic method abstract

model is constructed properties of the model are proven Set theory (and other discrete math) First order predicate calculus Schema calculus provides incrementality 6 Predicate Logic

Variables ranging over arbitrary sets Predicates: assertions about variables Operators: conjunction: A B disjunction: A B negation: A implication: A B

Quantifiers universal: x: T R(x) existential: x: T R(x) 7 Set Theory Membership: x S, x T Union: S T Intersection: S T

8 Functions and Relations element mapping: x y domain, range: dom(R), ran(R) overriding: R S partial function: x y 9

Sequences definition: <>, concatenation: length: #S functions: head(S) first element tail(S) all but the first element last(S) last element front(S) all but the last element

10 Schema Operators conjunction: S T disjunction: S T hiding: S \ (v1, , vn) hiding: S \ T overriding: S T

11 Names Variables input: name? output: name! postcondition: name'

Schema changes state: Name constant state: Name 12 Schemas Name declarations predicates

13 Birthday Book [Spivey 92] Example of use of schemas Describes a calendar with birthdates 14 BirthdayBook known: P NAME

birthday: NAME DATE known = dom birthday 15 Examples known = { Mark, Cheryl, Eric, Paul } birthday = { Mark

Cheryl July 9, Eric July 14, Paul April 30 April 7, } 16

AddBirthday BirthdayBook name? : NAME date? : DATE name? known birthday' = birthday {name? date?} 17

FindBirthday BirthdayBook name? : NAME date! : DATE name? known date! = birthday(name?) 18 Remind BirthdayBook today? : DATE

cards! : P NAME cards! = { n: known | birthday(n) = today? } 19 Initialization InitBirthday BirthdayBook known = 20

Deriving Properties known' = dom birthday' = dom ( birthday {name? date?} ) = dom birthday dom {name? date?} = dom birthday { name? } = known { name? }

21 Cartoon of the Day 22 Cartoon of the Day (cont.) 23 Symbol Table [Hayes 87] Describes a relation between symbols and

values Illustrates use of schema operators 24 Initial Definitions ST SYM st ST st0 VAL

25 Retrieve ST s? : SYM v! : VAL s? dom(st) v! = st(s?) 26

Declare ST s? : SYM v? : VAL st' = st { s? v? } 27 NotPresent ST

s? : SYM rep! : REPORT s? dom(st) rep! = "Symbol not present" 28 Success rep! : REPORT rep! = "OK" 29

Combining Schemas STRetrieve ( Retrieve Success) NotPresent STDeclare Declare Success 30 Overriding Definitions Introduce a new symbol table for each level of scope Need to override the previous definitions

of symbols: {s v} {s w} Need to introduce a distributed override operator for sequences of symbol tables 31 Block-Structured Symbol Tables BST seq ST

/ : seq ST ST / <> = / ( s < t > ) = (/ s ) t bst0 < > 32 BStart0 BST bst' = bst < st0 > BEnd0 BST

bst < > bst' = front( bst ) 33 Z Method 1. 2. 3. 4. 5. Introduce basic sets

Define an abstract state in terms of sets, functions, relations, sequences, etc. Specify the initial state Define pre- and post-conditions of operations State and prove theorems 34 References Ian Hayes (editor), Specification Case Studies, Prentice-Hall International, 1987, ISBN 0-13-826579-8.

J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall International, 1992, ISBN 0-13-978529-9. 35

Recently Viewed Presentations

  • Trade Promotion in Russia: Issues for Discussion*

    Trade Promotion in Russia: Issues for Discussion*

    What do we know about export promotion policies? Recent econometric evidence suggests that there are clear benefits from active export promotion - on average EPAs have a positive effect on exports (Lederman, 2010). There are, however, decreasing returns to scale...
  • Research using published sources - University College London

    Research using published sources - University College London

    Research using published sources Literature searching and bibliographic referencing Role of secondary sources in research: Some research will be totally dependent on published materials historical research overviews conceptual studies most research will require some use of published sources to provide...
  • Questions: Are you proud to be a part

    Questions: Are you proud to be a part

    Inherent problems: statistics show . although the composition of males versus females in the overall population are about even, approximately 75% of (school and library) administrators are men while 87% of elementary teachers are women and 61% of secondary teachers...
  • BEHAVIORAL FINANCE Behavioral finance, commonly defined as the

    BEHAVIORAL FINANCE Behavioral finance, commonly defined as the

    Investor irrationality has existed as long as the markets themselves have. Perhaps the best-known historical example of irrational investor behavior dates back to the early modern or mercantilist period during the sixteenth century. A man named Conrad Guestner transported tulip...
  • Thrombosis and Embolism

    Thrombosis and Embolism

    Myocardial Infarction (heart attack) Ischemia: tissue that has been starved of oxygen, but had not yet died It is possible to reverse ischemia with clot dissolving drugs Contains an enzyme that breaks down the clot What is the difference between...
  • Data-Driven Decision Making to Increase School-Completion Rates Todays

    Data-Driven Decision Making to Increase School-Completion Rates Todays

    Data Resources. ZoomWV/WV-eis a real-time, longitudinal data system that insures high-quality educational information.Helps drive educational initiatives to improve instruction and student performance in West Virginia, in part by making information available in easy-to-understand aggregate reports at the state, regional, county,...
  • Population Evolution - MS. SWISS AP BIOLOGY

    Population Evolution - MS. SWISS AP BIOLOGY

    Hardy Weinberg. Population: group of individuals of the same species, in the same area, that interbreed. Gene Pool: copies of every type of allele at every locus in all members of the population *Different from Punnett Squares- because we assume...
  • Figurative Language in To Kill a Mockingbird

    Figurative Language in To Kill a Mockingbird

    Figurative Language in Personification "Mr. Radley's older son lived in Pensacola; he came home at Christmas, and he was one of the few people we ever saw enter or leave the place. From the day Mr. Radley took Arthur home,...