Lecture Formal methods in software engineering - Lecture 30 presents the following content: OSI reference model, abstract state machine language (AsmL), abstract state, abstract state machine and turing machine, state transitions, evolution of state variables,. | Formal Methods in SE Lecture 30 OSI reference model Application Model-based specification Algebraic specification Abstract State Machine Language (AsmL) AsmL is a language for modelling the structure and behaviour of digital systems AsmL can be used to faithfully capture the abstract structure and step-wise behaviour of any discrete systems, including very complex ones such as: Integrated circuits, software components, and devices that combine both hardware and software Abstract State An AsmL model is said to be abstract because it encodes only those aspects of the system’s structure that affect the behaviour being modelled The goal is to use the minimum amount of detail that accurately reproduces (or predicts) the behaviour of the system Abstraction helps us reduce complex problems into manageable units and prevents us from getting lost in a sea of details AsmL provides a variety of features that allow you to describe the relevant state of a system in a very economical, high-level way Abstract State Machine and Turing Machine An abstract state machine is a particular kind of mathematical machine, like the Turing machine (TM) But unlike a TM, ASMs may be defined a very high level of abstraction An easy way to understand ASMs is to see them as defining a succession of states that may follow an initial state State transitions The behaviour of a machine (its run) can always be depicted as a sequence of states linked by state transitions Moving from state A to state B is a state transition paint in green paint in red A B Configurations Each state is a particular “configuration” of the machine The state may be simple or it may be very large, with complex structure But no matter how complex the state might be, each step of the machine’s operation can be seen as a well-defined transition from one particular state to another Evolution of state variables paint in green paint in red A B We can view any machine’s state as a dictionary of (Name, Value) pairs, called state . | Formal Methods in SE Lecture 30 OSI reference model Application Model-based specification Algebraic specification Abstract State Machine Language (AsmL) AsmL is a language for modelling the structure and behaviour of digital systems AsmL can be used to faithfully capture the abstract structure and step-wise behaviour of any discrete systems, including very complex ones such as: Integrated circuits, software components, and devices that combine both hardware and software Abstract State An AsmL model is said to be abstract because it encodes only those aspects of the system’s structure that affect the behaviour being modelled The goal is to use the minimum amount of detail that accurately reproduces (or predicts) the behaviour of the system Abstraction helps us reduce complex problems into manageable units and prevents us from getting lost in a sea of details AsmL provides a variety of features that allow you to describe the relevant state of a system in a very economical, high-level .
