| Titre : | Formal verification of the implementation of the MQTT protocol in IoT devices |
| Auteurs : | Aouatef Abid, Auteur ; Zohra Hamidi, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2019 |
| Format : | 1 vol. (56 p.) / ill. / 29 cm |
| Langues: | Anglais |
| Mots-clés: | Internet of Things (IoT),Message Queue Telemetry Transport (MQTT),formal verification,modular language TTCN-3. |
| Résumé : |
Internet of Things (IoT) is a technology used to provide smarter services to users by connecting various devices to the Internet and allowing these devices to exchange information with each other. This connections run out depending on certain protocols, including Message Queue Telemetry Transport (MQTT).MQTT is a protocol suitable for application in Internet of Things (IoT) devices; it is designed around requirements for low bandwidth and small code footprint. The count of the embedded devices that make use of it is constantly increasing. Therefore, a mistake in its implementation would be critical from both operational and security perspective. For that, we need to implement a program with new test language for verification of implementations of the MQTT protocol in IoT devices such as TTCN-3. the main objective of our work is to provide a formal verification of implementations of the MQTT protocol in IoT devices by using a modular language TTCN-3. |
| Sommaire : |
General introduction…………………………………………………………………... 1 « Chapter 1: Internet of things » 1. Introduction……………………………………………………………………...... 3 2. Internet of things (IoT)…………………………………………………………...... 3 2.1. Characteristics of the IoT…………………………………………………….... 5 2.2. IoT Application……………………………………………………………........ 6 2.3. IoT Standards and Protocols…………………………………………………... 7 2.3.1. Application Protocols…………………………………………………….. 9 a. Coap……………………………………………………………….................... 9 b. XMPP………………………………………………………………................. 10 c. AMQP………………………………………………………………................ 10 d. DDS………………………………………………………………..................... 10 e. MQTT…………………………………………….............................................. 11 3.2.2. Other protocols……………………………………………...........…........ 13 3. Advantages and Disadvantages of IoT…………………………………….……..... 17 4. IoT challenges…………………………………………………………………......... 19 5. Solutions for IoT…………………………………………………………………..... 20 6. Conclusion……………………………………………………………...................... 20 « Chapter 2: Software Testing » 1. Introduction………………………………………………………........................... 21 2. Software testing………………………………………………………………......... 21 3. Objectives of testing……………………………………………........ 21 4. Verification and Validation……………………………………………...…............ 21 5. Levels of testing………………………………………………...............………..... 22 5.1. Unit testing…………………………………………......................................... 22 5.2. Integration testing………………………………............................................... 22 5.3. System testing…………………………………..........................................…... 22 5.4. Acceptance testing…………………………………………………………….. 23 6. Categories of testing types…………………………………………………………. 23 6.1. Black box testing………………………………………………………………. 23 6.2. White box testing……………………………………………………………..... 24 6.3. Gray box testing……………………………………………………………....... 24 6.4. Non-Functional testing………………………………………………………..... 25 6.4.1. Performance testing……………………………………………………...... 25 6.4.2. Security testing…………………………………………………………..... 27 6.4.3. Recovery testing…………………………………………………………... 27 7. Limitations of testing………………………………………………………............. 28 8. TTCN-3 language………………………………………………………................ 28 8.1. Key TTCN-3 language features………………………………………........... 28 8.2. Language basics…………………………………………………………….. 29 8.3. The concepts of TTCN-3……………………………………………............. 30 8.3.1. Subtype………………………………………………………………..... 30 8.3.2. Components……………………………………………………......….... 30 8.3.3. Test case………………………………………………………............... 31 8.3.4. Templates……………………………………………………….............. 31 8.3.5. Alt statement………………………………………………………........ 32 9. Conclusion……………………………………………………………......................... 33 « Chapter 3: Conception and Implementation of system » 1. Introduction…………………………………………………………….................. 34 2. Structure of an MQTT control packet…………………………………………...... 34 3. MQTT message format………………………………………………………….... 35 3.1. Fixed header………………………………………………………….............. 35 3.2. Variable header………………………………………………………............. 39 3.3. Payload………………………………………………………………............. 40 4. Some of command message……………………………………………................. 41 4.1. CONNECT………………………………………………………………....... 41 4.2. PUBLISH………………………………………………………………......... 42 4.3.SUBSCRIBE………………………………………………………..............… 44 4.4. DISCONNECT…………………………………………………………........ 45 5. Development environment used.......................46 6. Deriving the test………………………………………………................……......47 7. Conclusion……………………………………………………………................... 54 General conclusion…………………………………………….......………………… 55 |
| Type de document : | Mémoire master |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/487 | Mémoire master | bibliothèque sciences exactes | Consultable |
