New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here

Formal Meth in Software Devel

by: Donnell Kertzmann

Formal Meth in Software Devel CSE 814

Donnell Kertzmann
GPA 3.97


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in Computer Science and Engineering

This 8 page Class Notes was uploaded by Donnell Kertzmann on Saturday September 19, 2015. The Class Notes belongs to CSE 814 at Michigan State University taught by Staff in Fall. Since its upload, it has received 45 views. For similar materials see /class/207424/cse-814-michigan-state-university in Computer Science and Engineering at Michigan State University.

Popular in Computer Science and Engineering


Reviews for Formal Meth in Software Devel


Report this Material


What is Karma?


Karma is the currency of StudySoup.

You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 09/19/15
Analytical modeling of software Lecture 3 Checking assertions Topics Exhaustive verification of assertions Classification hierarchies Time permitting execution traces cs5 em Formal Mather K mmwalt Generating instances and testing Program testing can be used to show the presence of bugs but never to show their absence 7 E W Dillltstra This is the fundamental problem in so ware testing 7 Eorahv l lOl lrlilvlal program the humoerordlstmct paths through the program is mtractaolv large 7 Not economical to develop tests for all of them or even to run such sts hce developed 7 elves l lSe to theories oftestrsulte adequacv and coverage Criterla Question In what way is instance generation similar to so ware testing cs5 em Formal Mather K mmwalt Exhaustive assertion verification Sometimes we would like to check that a property holds for all possible instances of a m d e E g m a banking application that the balance ofarl account can never go hegatve e E g whehevero e age tsehds a message is sent the intended recipient evehtuallv receives it Model checkers including the Alloy analyzer can do exactly this for nitestate models 7 conceptually the model checlltergeherates all possible lrrstarrces ofthe model and then goes and veri es that the propertv holds e in realltv exhaustive model generation is impractical 7 Tools explolt a varletv or optlmlzatlohs to avoid this cs5 em Formal Mather K mmwalt Assertions Defn A constraint that is intended to be valid e holds for all conceivable instances Example assert delUndoestd all b b b Book n name a Add addIbb na and delIb b 39 na implies badd b add cs5 em Formal Mather K mmwalt Assertion checking Assertions are checked rather than run Checking means checking that they do indeed follow from what was specified in the model ie that they are valid Example check delUndoesAdd for 3 Checks may generate a counterexample Note Checking is still bounded by a scope cs5 em Formal Mather K mmwalt Another example The following checks that delete is an undo for add e name did not already exist prior to adding Example assert delvndnesndd all h h h Hunk n llama a nddr 1 and delh h na implies haddr h addr cs5 em Formal Mather K mmwalt Small scope hypothesis Key assumption of Alloy Most flaws in a model can be revealed by a small instance thus an exhaustive analysis of small scopes should identify most if not all of the aws Question How does this assumption reconcile with ideas from software testing eat em FormalMathod K mrthzlt Classification hierarchies In a realistic address book application one can create address alias whose target is another alias create aliases with multiple targets Not possible to do this using the facilities we ve discussed thus far What is needed is the ability to define signature classification hierarchies eat em FormalMathod K mrthzlt Example Alloy model diagram eat em FormalMathod K mrthzlt Example touraddressBook2 abstract sig Target sig Addr extends Target abstract sig Name extends Target sig Alias Group extends Name sig Book addr Name gt Target Notes 7 Signature extension denotes a subset relation 7 Distinct extensions of sarne abstract signature are disioint a Extent ofari abstract signature is tne extent of its extensions eat em FormalMathod K mrthzlt Facts Notice Model currently allows an alias to be its wn target We can preclude this by adding a fact new constraint to the model fact all h Book no n Name ninnAbaddr eat em FormalMathod K mrthzlt Signature facts Previous fact could have been specified as part of the Book signature declaration sig Book addr Name gt Target non Name nin nMaddr eat em FormalMathod K mrthzlt CSE 814 Spring 04 Recall 0 We have seen hoW Alloy and FSP are useful in modeling designs and mechanically checking them for adherance to various properties 0 Additional needs 7 Integration With naturallanguage text 7 Scaling up Write speci cations With concepts that are easy to declare but too large to instantiate via automated tools 7 Modularizing speci cations to separate concerns 7 Re nement Relating an abstract speci cation to its implementation Recall 0 We have seen hoW Alloy and FSP are useful in modeling designs and mechanically checking them for adherance to various properties Additional needs 7 Integration With naturallanguage text 7 Scaling up Write speci cations With concepts that are easy to declare but too large to instantiate via automated tools 7 Modularizing speci cations to separate concerns 7 Re nement Relating an abstract speci cation to its implementation CSE 814 Spring 04 Z Schemas A Calculus for Composing and Manipulating Speci cations Z schema language 0 Z comprises two languages 7 The mathematical language of logic and sets and 7 The schema language 0 Schema language used to structure and compose descriptions 7 collating pieces of information 7 encapsulating these pieces and 7 naming them for reuse 0 Schema calculus used to derive new speci cations compute operation preconditions etc CSE 814 Spring 04 873 CSE 814 Spring 04 Notation 0 We Write schemas in either Namlng SChemaS 7 Horizontal form r 0 We may give names to schemasi declaration l constraint 0 These names abbreviate the corresponding pattern of 7 or Vertical form declaration and constraint o The de nition declaration Name 3 Exp constraint introduces a schema name Name that is equivalent to Exp Which must be a schema expression 0 ln vertical form we may omit the semicolons betW 1 1 een and the i quot between quot Examples Examples aZ clPZlc a c SchemaNamegaZ c2lPZlc3 Aa cl iC39L T aZ aZ c2llDZ c2llDZ cy g 69 aEc aEc CSE 814 Spring 04 Example Box o ice software 0 Given the basic types Castomer Seat 0 We can de ne the state of the box of ce which sells seats to customers i BoxO lce sold Seat 44 Customer seating PSeat dom sold Q seating 0 Review questions 7 Why is sold a partial function 7 Why is sold not an injection 0 To model the state of a text editor we rst need the set of all possible characters in the text CHAR Example Text editor 0 Then the editor contains one huge string called text and an insertion point indicating the point of focus within the text i Editor text seq CHAR insertion text y insertion E dom text U 0 0 Question What is the value of insertion when text sequence is empty 875 CSE 814 Spring 04 Composition and the Schema Calculus Schema inclusion 0 Most basic form of schema composition 0 Allows de nition of a new schema by extending an existing schema with additional declarations and constraints 0 The notation i S R declaration predicate declares S to be an extension of schema R 7 the declaration parts are added together 7 the constraints are conjoined o If the same variable name appears in both declaration parts the types must match CSE 814 Spring 04 Example Adding new declaration constraint 0 Suppose we want the state of our Editor to maintain the size in characters of the text 0 Using schema inclusion i Editor WithSize Editor size N size text 0 Question how would we have write this schema without using inclusion Example Adding new constraint 0 Schema inclusion is nice for partitioning a state space into a collection of disjoint modes 0 Consider the two modes Emptil Editor WithSize size 0 N onEmpty Editor WithSize CSE 814 Spring 04 Using Schemas to de ne Abstract State Models Formal de nition of a schema A schema expression denotes a set of special entities called bindings each of which is a mapping of schemavariable names to values The binding that associates the name of an identi er x with the value of expression 6 and the name of an identi er y with the value of f is written 4 96 M e y M f l Example G x a 2 y a 3 Schema expr denotes maximal set of bindings that are 7 well typed with respect to the schema declaration and 7 consistent with the schema constraint CSE 814 Spring 04 Schemas and state spaces 0 Each binding corresponds to a valid state of a system declared using a schema 7 declaration part describes conceivable states 7 constraints limit the conceivable states to a subset of admissible states 0 Example i UpperT riangula r x N y2N xlty 0 Thus the schema declares a space or set of such states Conceivable states of UpperTriangular lt H10 mmgHmlt Values of X CSE 814 Spring 04 lt H10 mmgHmlt Admissible states of UpperTriangular 2 3 4 Values of X Schemabased speci cation Conceivable States gt Admissible States CSE 814 Spring 04 Schema inclusion and admissible states 0 We can understand schema inclusion in terms of admissible states 0 Example UP Upper Triangular xmod20 Odd Upper Triangular Example Even V 4 a 1 u 3 e s 2 o f 1 Y o o 1 2 3 4 Values of X 8711 CSE 814 Spring 04 Example Odd V a 1 u e s o f Y o 1 2 3 4 Values of X Schema inclusion revisited 0 When schema inclusion is used to add constraints the admissible states in a speci cation can be partitioned o Often systems have intuitive high level77 states Which can be characterized by a subset of the admissible states 0 We can use these intuitive states to modularize our speci cation


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

Why people love StudySoup

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

Amaris Trozzo George Washington University

"I made $350 in just two days after posting my first study guide."

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.