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

  • Capital Structure in a Perfect Market Chapter 14

    Capital Structure in a Perfect Market Chapter 14

    MM Proposition II: The cost of capital of levered equity is equal to the cost of capital of unlevered equity plus a premium that is proportional to the market value debt-equity ratio. Modigliani - Miller. Back to our example.
  • Day 8 - Mr. London&#x27;s Science Classes

    Day 8 - Mr. London's Science Classes

    A. dissection of the flowers of both tall and short African violet plants . B. microscopic observation of the nuclei of fruit fly cells . C. biochemical analysis of DNA produced in the F2 generations of roan cattle . D....
  • Political Spectrum and Canadian political parties

    Political Spectrum and Canadian political parties

    The political spectrum is divided into "Left" and "Right" The division is based off of the seating of members newly . elected . to the French Legislated Assembly in 1791- during the French . Revolution. King Louis XVI. The Left:...
  • Senior Parent Night - Edl

    Senior Parent Night - Edl

    Types of Financial Aid. Grants: Money that is mostly awarded on the basis of need and DOES NOT have to be repaid.. Work Study: Programs of on or off-campus jobs for students who demonstrate financial need. Hours are limited. Loans
  • Fracture Femur - Kmc

    Fracture Femur - Kmc

    Two cm shorting and up to 20 degrees angulation is accepted in children but again no rotation. Complications - Malunion - Leg length discrepancy usually shortening but may be increase in length due to 1- Active healing process( hyperaemia and...
  • Schoology at GRMS

    Schoology at GRMS

    Schoology at FCMS. Schoology is a new communication platform for teachers, students, and parents. We hope this will assist in creating a culture at GRMS that helps our community feel welcome, valued, involved, and informed.
  • ABACUS 4th Century B.C. The abacus, a simple

    ABACUS 4th Century B.C. The abacus, a simple

    BLAISE PASCAL (1623 - 1662) Originally called a "numerical wheel calculator" or the "Pascaline", Pascal's invention utilized a train of 8 moveable dials or cogs to add sums of up to 8 figures long. As one dial turned 10 notches...
  • Lecture Goals  To discuss why nitrogen and phosphorus

    Lecture Goals To discuss why nitrogen and phosphorus

    The Nutrient Spiraling Model P Estimating S S Low = Retentive S High = Leaky Labeled Nutrient (e.g., PO43- or NO3-) + Inert Tracer (e.g., Br or Cl) Concentration Downstream Nutrient Tracer Why are N and P important? N and...