Formal Meth in Software Devel
Formal Meth in Software Devel CSE 814
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.
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
Are you sure you want to buy this material for
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'