Skip to main content
SpringerLink
Log in

Improving Formal Verification and Testing Techniques for Internet of Things and Smart Cities

  • Published:
Mobile Networks and Applications Aims and scope Submit manuscript

Abstract

We are interested in formal verification and model-based testing for Internet of Things and Smart Cities. In general these two techniques suffer from state explosion problem. To remedy this situation we propose a set of techniques which aim to reduce the cost, duration and complexity of the considered problems. On the first hand the techniques realted to formal verification are as follows. First, Abstraction consists in modelling a part of the system accurately and the other parts at high level. Second, Modularization and Compositionality consist in splitting the whole system into smaller subsystems. Third, Symmetry Detection exploits symmetries that take place during the system execution. Fourth, Data Independence consists in detecting that the behaviour of the considered system does not depend on some data inputs. Fifth, Eliminating Functional Dependencies consists in removing dependency among state variables. Sixth, Exploiting Reversible Rules consists in collapsing subgraphs of the graph of states into abstract states. On the second hand the techniques related to model-based testing are as follows. First, Refinement Techniques extract test scenarios directly from the untimed specification. Second, the Reduction of the Size of Digital-Clock Tests Technique provides a heuristic to reduce the size of the generated tests. Third, the Timed Automata Testers Generation Technique allows to produce testers in the form of deterministic timed automata. Fourth, the Test Cases Updating Technique after System Evolution makes it possible to reduce the number of tests to be generated after each adaptation. Fifth, the Resource Aware Test Component Placement Technique allows to produce a placement plan of the different testers. Sixth, Coverage Technique generates a reasonable-size set of tests. A case study is proposed in order to illustrate the use of these techniques.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Notes

  1. This article is an extension of our previous work [27] presented in SCITA 2017 [38]

References

  1. Alam F, Mehmood R, Katib I (2020) Comparison of decision trees and deep learning for object classification in autonomous driving. Springer International Publishing, Cham, pp 135–158. https://doi.org/10.1007/978-3-030-13705-2_6

    Google Scholar 

  2. Alam F, Mehmood R, Katib I, Albeshri A (2016) Analysis of eight data mining algorithms for smarter internet of things (iot). Proc Comput Sci 98:437–442. https://doi.org/10.1016/j.procs.2016.09.068. http://www.sciencedirect.com/science/article/pii/S187705091632213X. The 7th International Conference on Emerging Ubiquitous Systems and Pervasive Networks (EUSPN 2016)/The 6th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH-2016)/Affiliated Workshops

    Article  Google Scholar 

  3. Alam F, Mehmood R, Katib I, Albogami NN, Albeshri A (2017) Data fusion and iot for smart ubiquitous environments: A survey. IEEE Access 5:9533–9554. https://doi.org/10.1109/ACCESS.2017.2697839

    Article  Google Scholar 

  4. Alamoudi E, Mehmood R, Albeshri A, Gojobori T (2020) A survey of methods and tools for large-scale DNA mixture profiling. Springer International Publishing, Cham, pp 217–248. https://doi.org/10.1007/978-3-030-13705-2_9

    Google Scholar 

  5. Albino V, Berardi U, Dangelico R (2015) Smart cities: Definitions, dimensions, performance, and initiatives. J Urban Technol 22:3–21

    Article  Google Scholar 

  6. Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126:183–235

    Article  MathSciNet  Google Scholar 

  7. Andraus ZS, Sakallah KA (2004) Automatic abstraction and verification of verilog models. In: Proceedings of the 41st annual design automation conference, DAC ’04. ACM, New York, pp 218–223. https://doi.org/10.1145/996566.996629

  8. Aqib M, Mehmood R, Alzahrani A, Katib I, Albeshri A, Altowaijri SM (2019) Rapid transit systems: Smarter urban planning using big data, in-memory computing, deep learning, and gpus. Sustainability 11(10). https://doi.org/10.3390/su11102736. https://www.mdpi.com/2071-1050/11/10/2736

  9. Aqib M, Mehmood R, Alzahrani A, Katib I, Albeshri A, Altowaijri SM (2019) Smarter traffic prediction using big data, in-memory computing, deep learning and gpus Sensors 19(9). https://doi.org/10.3390/s19092206

  10. Benalycherif L, McIsaac A (2009) A semantic condition for data independence and applications in hardware verification. Electron Notes Theor Comput Sci 250(1):39–54. https://doi.org/10.1016/j.entcs.2009.08.004. http://www.sciencedirect.com/science/article/pii/S1571066109003296. Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS 2007)

    Article  Google Scholar 

  11. Bensalem S, Krichen M, Majdoub L, Robbana R, Tripakis S (2007) A simplified approach for testing real-time systems based on action refinement. In: ISoLA, Revue des Nouvelles Technologies de l’Information, vol. RNTI-SM-1, pp. 191–202. Cėpaduės-Ėditions

  12. Bertot Y, Castran P (2010) Interactive theorem proving and program development: Coq’Art the calculus of inductive constructions, 1st edn, Springer Publishing Company, Incorporated

  13. Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality, LNCS, vol 1536. Springer

  14. Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in c. IEEE Trans Softw Eng 30(6):388–402. https://doi.org/10.1109/TSE.2004.22

    Article  Google Scholar 

  15. Lee C-C, Jiang JR, Huang C-Y, Mishchenko A (2007) Scalable exploration of functional dependency by interpolation and incremental sat solving. In: 2007 IEEE/ACM international conference on computer-aided design, pp 227–233, DOI https://doi.org/10.1109/ICCAD.2007.4397270

  16. Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, workshop. Springer-Verlag, Berlin, pp 52–71. http://dl.acm.org/citation.cfm?id=648063.747438

  17. Emerson EA, Wahl T (2005) Dynamic symmetry reduction. In: Halbwachs N, Zuck LD (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 382–396

  18. Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, New York

    Google Scholar 

  19. Hessel A, Larsen K, Nielsen B, Pettersson P, Skou A (2003) Time-optimal real-time test case generation using UPPAAL. In: FATES’03

  20. Hu AJ, Dill DL (1993) Reducing bdd size by exploiting functional dependencies. In: 30th ACM/IEEE design automation conference, pp 266–271. https://doi.org/10.1145/157485.164888

  21. Iosif R (2002) Symmetry reduction criteria for software model checking. In: Bošnački D, Leue S (eds) Software, model checking. Springer, Berlin, pp 22–41

  22. Ip CN (1998) Generalized reversible rules. In: Proceedings of the 2nd international conference on formal methods in computer-aided design, FMCAD ’98. Springer-Verlag, London, pp 403–420. http://dl.acm.org/citation.cfm?id=646185.758715

  23. Ip CN, Dill DL State reduction using reversible rules. In: Proceedings of the 33st Conference on Design Automation, Las Vegas, Nevada, USA, Las Vegas Convention Center, June 3-7, 1996., pp 564–567 1996. https://doi.org/10.1145/240518.240625

  24. Jiang JHR, Brayton RK (2004) Functional dependency for verification reduction. In: Alur R, Peled DA (eds) Computer aided verification. Springer, Berlin, pp 268–280

  25. Kesten Y, Pnueli A, Zlatuška J (1998) Modularization and abstraction: The keys to practical formal verification. In: Brim L, Gruska J (eds) Mathematical foundations of computer science 1998. Springer, Berlin, pp 54–71

  26. Krichen M (2012) A formal framework for black-box conformance testing of distributed real-time systems. IJCCBS 3(1/2):26–43. https://doi.org/10.1504/IJCCBS.2012.045075

    Article  Google Scholar 

  27. Krichen M, Cheikhrouhou O, Lahami M, Alroobaea R, Jmal Maâlej A. (2018) Towards a model-based testing framework for the security of internet of things for smart city applications. In: Mehmood R, Bhaduri B, Katib I, Chlamtac I (eds) Smart societies, infrastructure, technologies and applications. Springer International Publishing, Cham, pp 360–365

  28. Krichen M, Maâlej AJ, Lahami M (2018) A model-based approach to combine conformance and load tests: an ehealth case study. IJCCBS 8(3/4):282–310. https://doi.org/10.1504/IJCCBS.2018.096437

    Article  Google Scholar 

  29. Krichen M, Tripakis S Black-box conformance testing for real-time systems. In: 11th international spin workshop on model checking of software (SPIN’04), LNCS, vol. 2989. Springer (2004). Available at http://www-verimag.imag.fr/PEOPLE/Stavros.Tripakis/papers/timetest.pdf

  30. Krichen M, Tripakis S (2009) Conformance testing for real-time systems. Formal Methods in System Design 34(3):238–304

    Article  Google Scholar 

  31. Kripke SA (1963) Semantical considerations on modal logic. Acta Philosophica Fennica 16(1963):83–94

    MathSciNet  Google Scholar 

  32. Kwiatkowska M, Norman G, Parker D (2006) Symmetry reduction for probabilistic model checking. In: Ball T, Jones RB (eds) Computer aided verification. Springer, Berlin, pp 234–248

  33. Lahami M, Fakhfakh F, Krichen M, Jmaïel M (2012) Towards a TTCN-3 test system for runtime testing of adaptable and distributed systems. In: Proceedings of the 24th IFIP WG 6.1 international conference testing software and systems (ICTSS’12), pp 71–86

  34. Lahami M, Krichen M, Barhoumi H, Jmaiel M (2015) Selective test generation approach for testing dynamic behavioral adaptations. In: Testing software and systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Sharjah and Dubai, United Arab Emirates, November 23-25, 2015, Proceedings, pp 224–239. https://doi.org/10.1007/978-3-319-25945-1_14

  35. Lahami M, Krichen M, Bouchakwa M, Jmaïel M (2012) Using knapsack problem model to design a resource aware test architecture for adaptable and distributed systems. In: Proceedings of the 24th IFIP WG 6.1 international conference testing software and systems (ICTSS’12), pp. 103–118

  36. Maȧlej AJ, Lahami M, Krichen M, Jmaïel M (2018) Distributed and resource-aware load testing of WS-BPEL compositions. In: ICEIS (2), pp. 29–38. SciTePress

  37. Mehmood R, Graham G (2015) Big data logistics: A health-care transport capacity sharing model. Proc Comput Sci 64:1107–1114. http://www.sciencedirect.com/science/article/pii/S1877050915027015. Conference on ENTERprise Information Systems/International Conference on Project MANagement/Conference on Health and Social Care Information Systems and Technologies, CENTERIS/ProjMAN / HCist 2015 October 7–9, 2015, https://doi.org/10.1016/j.procs.2015.08.566

    Article  Google Scholar 

  38. Mehmood R, Katib I, Chlamtac I, Bhaduri B (2018) Smart societies, infrastructure, technologies and applications: First international conference, SCITA 2017, Jeddah, Saudi Arabia, November 27–29, 2017, Proceedings, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 224) Springer. https://doi.org/10.1007/978-3-319-94180-6

  39. Momtahan L (2005) Towards a small model theorem for data independent systems in alloy. Electron Notes Theor Comput Sci 128(6):37–52. https://doi.org/10.1016/j.entcs.2005.04.003. http://www.sciencedirect.com/science/article/pii/S1571066105002355. Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS 2004)

    Article  Google Scholar 

  40. Muhammed T, Mehmood R, Albeshri A, Alzahrani A (2020) HCDSR: A hierarchical clustered fault tolerant routing technique for IoT-based smart societies. Springer International Publishing, Cham, pp 609–628. https://doi.org/10.1007/978-3-030-13705-2_25

    Google Scholar 

  41. Muhammed T, Mehmood R, Albeshri A, Katib I (2018) Ubehealth: A personalized ubiquitous cloud and edge-enabled networked healthcare system for smart cities. IEEE Access 6:32258–32285. https://doi.org/10.1109/ACCESS.2018.2846609

    Article  Google Scholar 

  42. Myers G (1979) The art of software testing. Wiley

  43. Neto ACD, Travassos GH (2010) A picture from the model-based testing area: Concepts, techniques, and challenges. Adv Comput 80:45–120

    Article  Google Scholar 

  44. Nielsen B, Skou A (2001) Automated test generation from timed automata. In: TACAS’01. LNCS 2031, Springer

  45. Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, vol 2283. Springer

  46. Norris IPC, Dill DL (1996) Better verification through symmetry. Formal Methods in System Design 9 (1):41–75. https://doi.org/10.1007/BF00625968

    Article  Google Scholar 

  47. Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th colloquium on international symposium on programming. http://dl.acm.org/citation.cfm?id=647325.721668. Springer-Verlag, London, pp 337–351

  48. Roscoe AW, Broadfoot PJ (1999) Proving security protocols with model checkers by data independence techniques. J Comput Secur 7(1):147–190. http://content.iospress.com/articles/journal-of-computer-security/jcs120

    Article  Google Scholar 

  49. Schlingensiepen J, Mehmood R, Nemtanu FC, Niculescu M (2014) Increasing sustainability of road transport in european cities and metropolitan areas by facilitating autonomic road transport systems (arts). In: Wellnitz J, Subic A, Trufin R (eds) Sustainable automotive technologies 2013. Springer International Publishing, Cham, pp 201–210

  50. Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: 13th annual symposium on theoretical aspects of computer science, STACS’96, LNCS, vol 1046. Spinger-Verlag

  51. Söderström O, Paasche T, Klauser F (2014) Smart cities as corporate storytelling. City: analysis of urban trends 18. https://doi.org/10.1080/13604813.2014.906716

  52. Springintveld J, Vaandrager F, D’Argenio P (2001) Testing timed automata. Theoretical Computer Science 254

  53. Thacker RA, Jones KR, Myers CJ, Zheng H (2010) Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the 1st ACM/IEEE international conference on cyber-physical systems, ICCPS ’10. ACM, New York, pp 12–21, DOI https://doi.org/10.1145/1795194.1795197

  54. Tretmans J (1992) A formal approcah to conformance testing. Ph.D. thesis, University of Twente Twente The Netherlands

  55. Utting M, Pretschner A, Legeard B (2012) A taxonomy of model-based testing approaches. Softw Test Verif Reliab 22(5):297–312. https://doi.org/10.1002/stvr.456

    Article  Google Scholar 

  56. Velev MN (2001) Automatic abstraction of memories in the formal verification of superscalar microprocessors. In: Margaria T, Yi W (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 252–267

  57. Wahl T, Donaldson A (2010) Replication and abstraction: Symmetry in automated formal verification. Symmetry 2(2):799–847. https://doi.org/10.3390/sym2020799

    Article  MathSciNet  Google Scholar 

  58. Lee W, Pardo A, Jang J-Y, Hachtel G, Somenzi F (1996) Tearing based automatic abstraction for ctl model checking. In: Proceedings of international conference on computer aided design, pp 76–81, DOI https://doi.org/10.1109/ICCAD.1996.568969

  59. Zhang J, Goldsby HJ, Cheng BH (2009) Modular verification of dynamically adaptive systems. In: Proceedings of the 8th ACM international conference on aspect-oriented software development, AOSD ’09. ACM, New York, pp 161–172, DOI https://doi.org/10.1145/1509239.1509262

  60. Zhu H, Belli F (2009) Advancing test automation technology to meet the challenges of model-based software testing - guest editors’ introduction to the special section of the third IEEE international workshop on automation of software test (AST 2008). Inf Softw Technol 51(11):1485–1486

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of CSIT, Al-Baha University, Al-Baha, Saudi Arabia

    Moez Krichen

  2. ReDCAD Laboratory, University of Sfax, Sfax, Tunisia

    Moez Krichen

Authors
  1. Moez Krichen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Moez Krichen.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Krichen, M. Improving Formal Verification and Testing Techniques for Internet of Things and Smart Cities. Mobile Netw Appl 28, 732–743 (2023). https://doi.org/10.1007/s11036-019-01369-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11036-019-01369-6

Keywords

Search

Navigation