Đang chuẩn bị liên kết để tải về tài liệu:
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.parent = o.~contents.~entries} inv UniqueNames {all d | all e1, e2: d.entries | e1.name = e2.name -> e1 = e2} inv Parents { no Root.parent all d: Dir – Root | one d.parent} inv Acyclic {no d | d in d.+parent} inv Reachable {Object in Root.*children} cond TwoDeep {some Root.children.children} assert FileHasEntry {all o | sole o.parent} assert AtMostOneParent {all o | sole o.parent} 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