Abstract Model SpecificationSlide 2NotationFeatures( Z-notation)SchemaSchema(cont.)Notation - ExampleExampleExample(cont.)Race conditionOperatorsLogical Conjunction OperatorLogical Disjunction operatorUse of OperatorsFrom specification to designData RefinementExample(Data and Direct Refinement)AdvantagesChemical Abstract ModelFeatures(CHAM)Alloy: A Lightweight Object Modeling NotationIntroductionSlide 23Example (File System)Slide 25AnalysisBased On ZFeaturesDesign FaultsFormalizing Style to Understand Descriptions of Software ArchitectureSlide 31Slide 32How is it done?Slide 34Abstract Syntax of Software ArchitecturesSlide 36Slide 37Step 1 (Define Semantic Model)Slide 39Step 2Step 3Step 4Slide 431Abstract Model SpecificationTarang Garg Srikumar Nagaraj2Abstract Model Specification•Explicitly describes behavior in terms of a model using well-defined types (viz. set, sequences, relations, functions) & defines operations by showing effects on model•Specification includes•type - syntax of object being specified•model - underlying structure•invariant - properties of modeled object•pre/post conditions – semantics of operations3 Notation•Is used to test the results•Independent of program code•Mathematical Data model•Represent both static and dynamic aspects of a system4Features( Z-notation)•Decompose specification into small pieces (Schemas)•Schemas are used to describe both static and dynamic aspects of a system•Data Refinement•Direct Refinement•You can ignore details in order to focus on the aspects of the problem you are interested in5SchemaStatic Aspect The state can occupy.The invariant relationships that are maintained as the system moves from state to state6Schema(cont.)Dynamic Aspect The operations that are possibleThe relationship between their inputs and outputs.The change of state that happen.7Notation - ExampleSome variables are declared. Relationship between the values of the variablesNameInit Birthday BookKnown = Birthday Book8ExampleBirthday bookknown: NAMEbirthday: NAME DATEKnown : dom birthdayAdd BirthdayBirthday Bookname?: NAMEdate?: DATEname? knownbirthday’ = birthday { name? date}9Example(cont.)Find Birthday Birthday bookname?: NAMEdate? : DATEname? Known date != birthday(name?)10Race conditionWe have not handled the condition when user tries to add a birthday, which is already known to the system, or tries to find the birthday of someone not known.Handle this by adding an extra result! To each operation. Result := of| already_known | not_knownSuccessResult! : REPORTResult! = ok11Operators (Conjunction of the two predicate parts) – any common variables of the two schemas are mergedV (the effect of the schema operator is to make a schema in which the predicate part is the result of joining the predicate parts of its two arguments with the logical connective V).12Logical Conjunction OperatorThe conjunction operator of the schema calculus allows us to combine this description with our previous description of AddBirthdayAddBirthday SuccessThis describes an operation which, for correct input, both acts as described by AddBirthday and produces the result ok.13Logical Disjunction operatorThis declaration specifies that if error occurs, the state of the system should not change.Robust version of AddBirthday can beRAddBirthday (AddBirthday Success) V AlreadyknownAlreadyKnown BirthdayBookname? : NAMEresult?: REPORTName? knownResult! = already_known14 Use of OperatorsRAdd BirthdayBirthday Bookname?: NAMEdate?: DATEresult!: REPORT(name? known birthday’= birthday {name? Date?} result!= ok) V (name? known birthday’ = birthday result != already_known)15Data Refinement“ to describe the concrete data structures which the program will use to represent the abstract data in the specification, and to derive description of the operation in terms of the concrete data structures”Direct Refinement: method to go directly from abstract specification to program in one stepFrom specification to design16Data RefinementData Structures: Two arrays : names [1…] of NAME dates [1…] of DATESnames’ = names{i v} ; names[i] := vthe right side of this equation is a function which takes the same value as names everywhere except at the argument i, where it takes the value ‘v’.17Example(Data and Direct Refinement)FindBirthday1 BirthdayBook1 name?:NAME date?:DATEi : 1.. hwmname?=names(i) date! = dates(i)Procedure FindBirthday(name: NAME; var date : DATE);var i: INTEGER;begini:=1;while names[i] name do i := i+1;dates := dates[i]end;18AdvantagesThe flexibility to model a specification which can directly lead to the code.Easy to understandA large class of structural models can be described in Z without higher – order features, and can thus be analyzed efficiently.Independent Conditions can be added later19Chemical Abstract ModelCHAM: for architectural description and analysis. Software Systems chemicals (whose reactions are controlled by explicitly stated rules).Where floating molecules can only interact according to a stated set of reaction rules.20Features(CHAM)- Modular specification-Chemical reactions-Molecules (components)-Reactions (Connectors)-Solutions (States of CHAM)-This is used in areas where intended architecture will tend to be large, complex, and assembled from existing components.-Architectural elements: Processing elements, data elements, and connecting elements.21Alloy: A Lightweight Object Modeling Notation22Introduction•Alloy–Is a modeling notation that describes structural properties–Has a declaration syntax compatible with graphical object models–Has a “set-based” formula syntax–Is based on “Z”23ExampleFile SystemDirEntry NameObject contents!name!Parent(~children)entries!DirFileRoot!24Example (File System)model FileSystem {domain {Object, DirEntry, fixed Name}state {partition File, Dir: static ObjectRoot: fixed Dir!entries: Dir! -> DirEntryname: DirEntry -> static Name!contents: DirEntry -> static Object!parent (~children) : Object -> Dir }def parent {all o | o.parent = o.~contents.~entries}inv UniqueNames {all d | all e1, e2: d.entries | e1.name = e2.name -> e1 = e2}inv Parents {no Root.parentall d: Dir – Root | one d.parent}inv Acyclic {no d | d in d.+parent}inv Reachable {Object in Root.*children}cond TwoDeep {some
View Full Document
Unlocking...