Model-based techniques for verification and validation require a model of the system under test (SUT). However, most communication systems lack a complete, correctmodel. One approach for generating a model of a system is to infer the model byobserving its external behavior. This approach is useful when the source code of thesystem is not available, e.g., third party components. Regular inference techniques areable to infer a finite state machine model of a system by observing its externalbehavior.In this master thesis we consider the models inferred by regular inferencetechniques of a certain kind of systems: communication protocol entities. Suchentities interact by sending and receiving messages consisting of a message type and anumber of parameters, each of which potentially can take on a large number of values.This may cause a model of a communication protocol entity inferred by regularinference, to be very large. Since regular inference creates a model from the observedbehavior of a communication protocol entity, the model may be very different from adesigner’s model of the system’s source code.This master thesis presents a novel approach to transform the inferred model ofcommunication protocols to a new formalism in a sense that it is more compact andit has a similar partitioning of an entity’s behavior into control states as in…
Contents
1 Introduction
1.1 General Information
1.2 Problem Description
1.2.1 Background
1.2.2 Aims and Objectives
1.2.3 Tasks
1.3 Prerequisites
1.4 Report Structure
2 Background
2.1 Communication Protocols
2.2 Verification
2.2.1 Testing
2.2.2 Formal Verification
2.2.3 Testing vs. Formal Verification
2.2.4 Theorem Proving
2.2.5 Model Checking
2.3 Models
2.3.1 Deterministic Finite-State Automaton
2.3.2 Mealy Machine
2.4 Symbolic Representation of Mealy Machines for Communica-tion Protocols
2.4.1 Input and Output Symbols
2.4.2 State Variables
2.4.3 Action Expressions
2.4.4 Definition of Symbolic Mealy Machine
2.5 Regular Inference
2.5.1 Anguelin’s Algorithm L
2.5.2 Regular Inference for Mealy Machines
3 Methodology
3.1 Transformation of Mealy Machines to Symbolic Mealy Machines
3.1.1 State Variables
3.1.2 Forming Locations
3.1.3 Action Expression Generation
3.1.4 Merging Locations
3.2 Complete Algorithm
3.2.1 Relations
3.2.2 Relational Operations
3.2.3 Forming Locations
3.2.4 Action Expressions
3.2.5 Pseudo Code
4 Implementation
4.1 ARFF File Format
4.2 Implementation of Our Tool
4.2.1 C4.5 Algorithm
4.2.2 Weka
5 Experiments
5.1 A-MLC
5.2 Inference of Mealy Machine Model
5.2.1 LearnLib
5.2.2 Inferred Mealy Machine
5.3 Running Our Tool
5.4 Result
5.4.1 Evaluation
6 Conclusion and Future Work
6.1 Discussion
6.2 Conclusion
6.3 Future Works
Author: Soleimanifard, Siavash
Source: Uppsala University Library
Download URL 2: Visit Now