TAILIEUCHUNG - Lecture Formal methods in software engineering - Lecture 18: Abstract model specification

In this chapter, the following content will be discussed: Abstract model specification, notation, features( Z-notation), the state can occupy, the invariant relationships that are maintained as the system moves from state to state, the operations that are possible, the relationship between their inputs and outputs, the change of state that happen. | Formal Methods in SE Abstract Model Specification Lecture # 18 Abstract 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 operations Notation Is used to test the results Independent of program code Mathematical Data model Represent both static and dynamic aspects of a system Features( 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 in Schema Static Aspect The state can occupy. The invariant relationships that are maintained as the system moves from state to state Schema(cont.) Dynamic Aspect The operations that are possible The relationship between their inputs and outputs. The change of state that happen. Notation - Example Some variables are declared. Relationship between the values of the variables Name Init Birthday Book Known = Birthday Book Example Birthday book known: NAME birthday: NAME DATE Known : dom birthday Add Birthday Birthday Book name?: NAME date?: DATE name? known birthday’ = birthday { name? date} Example(cont.) Find Birthday Birthday book name?: NAME date? : DATE name? Known date != birthday(name?) Race condition We 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

• Kỹ thuật lập trình
• Software engineering
• Formal methods in software engineering
• Software development methods
• Formal languages
• Automata theory
• Abstract model specification
• Object oriented software engineering
• Practical software development
• Object orientation
• Software quality
• Software engineering projects
• Introduction to software engineering
• Lecture Introduction to software engineering
• Công nghệ phần mềm
• Software process
• Software engineering ethics
• Lecture Software engineering
• Professional software development
• Software process activities
• Software engineering diversity
• Introduction Software Engineering
• Software products
• FAQs about software engineering
• Essential attributes of good software
• Importance of software engineering
• Software processes
• Aspect oriented software engineering
• The separation of concerns
• Software engineering with aspects
• Quality concepts
• Detail Design
• Design Software Engineering
• Implementation Software Engineering
• Build Software Engineering
• Buy Software Engineering
• Requirement engineering
• Requirement engineering process
• Software requirements engineering
• Lecture Software requirements engineering
• Requirements engineering
• Software requirements engineering
• Lecture Software requirements engineering
• System engineering
• Software requirements document
• Requirements engineering process tasks