tailieunhanh - Lecture Formal methods in software engineering - Lecture 19: Abstract model specification (cont)

Lecture Formal methods in software engineering - Lecture 19: Abstract model specification. In this chapter, the following content will be discussed: Chemical abstract model, structure of the model, automatic analysis, formalizing style to understand descriptions of software architecture,. | Formal Methods in SE Abstract Model Specification Lecture # 19 Advantages The flexibility to model a specification which can directly lead to the code. Easy to understand A 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 later Chemical Abstract Model CHAM: 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. Features(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. Alloy: A Lightweight Object Modeling Notation Introduction 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” Example File System DirEntry Name Object contents ! name ! Parent (~children) entries ! Dir File Root! Example (File System) model FileSystem { domain {Object, DirEntry, fixed Name} state { partition File, Dir: static Object Root: fixed Dir! entries: Dir! -> DirEntry name: DirEntry -> static Name! contents: DirEntry -> static Object! parent (~children) : Object -> Dir } def parent {all o | = o.~contents.~entries} inv UniqueNames {all d | all e1, e2: | = -> e1 = e2} inv Parents { no all d: Dir – Root | one } inv Acyclic {no d | d in d.+parent} inv Reachable {Object in Root.*children} cond TwoDeep {some } assert FileHasEntry {all o | sole } assert AtMostOneParent {all o | sole } op NewDirEntries | Formal Methods in SE Abstract Model Specification Lecture # 19 Advantages The flexibility to model a specification which can directly lead to the code. Easy to understand A 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 later Chemical Abstract Model CHAM: 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. Features(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. Alloy: A Lightweight Object Modeling Notation