Skip to main content
SpringerLink
Log in
Book cover

Smart and Digital Cities pp 287–309Cite as

Critical Systems for Smart Cities: Towards Certifying Software

  • Chapter
  • First Online:

  • 755 Accesses

Part of the book series: Urban Computing ((UC))

Abstract

Critical systems require high reliability and are present in many applications. Standard techniques of software engineering are not enough to ensure the absence of unacceptable failures and/or that critical requirements are fulfilled. Verifying and certifying systems for Smart Cities is one of the challenges that still require some effort. Smart Cities models may be seen as Cyber-Physical Systems and they may be formalized as Finite State Machines. We discuss how to reason over these models as Finite State Machines formalized in a logical background from which it is possible to provide certified software for the Smart Cities domain.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    https://www.nytimes.com/2018/03/19/technology/uber-driverless-fatality.html.

  2. 2.

    https://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/.

  3. 3.

    http://github.com/simasgrilo/RGCoq.

  4. 4.

    https://coq.inria.fr/library/Coq.Lists.ListSet.html.

  5. 5.

    https://coq.inria.fr/refman/program.html.

  6. 6.

    https://coq.inria.fr/library/Coq.Classes.EquivDec.html.

  7. 7.

    https://coq.inria.fr/refman/extraction.html.

  8. 8.

    More realistic fuel decreasing functions may be modelled, such as an exponential decreasing based on time, topography, etc.

References

  1. Ai, Y., Peng, M., Zhang, K.: Edge computing technologies for internet of things: a primer. Digital Commun. Netw. 4(2), 77–86 (2018)

    Article  Google Scholar 

  2. Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)

    Article  MathSciNet  Google Scholar 

  3. Arbab, F.: Coordination for component composition. Electron. Notes Theor. Comput. Sci. 160, 15–40 (2006). Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005)

    Google Scholar 

  4. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2013)

    MATH  Google Scholar 

  5. Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Model checking flight control systems: the airbus experience. In: 31st International Conference on Software Engineering-Companion Volume, 2009. ICSE-Companion 2009, pp. 18–27. IEEE, Piscataway (2009)

    Google Scholar 

  6. Cassandras, C.G.: Smart cities as cyber-physical social systems. Engineering 2(2), 156–158 (2016)

    Article  Google Scholar 

  7. de Souza Silva, N.: Verificação formal de sistemas embarcados em carro elétrico. Master’s thesis, Universidade Federal de Goiás (2015)

    Google Scholar 

  8. Derler, P., Lee, E.A., Vincentelli, A.S.: Modeling cyber–physical systems. Proc. IEEE 100(1), 13–28 (2012)

    Article  Google Scholar 

  9. Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., Werner, B.: The COQ Proof Assistant: User’s Guide: Version 5.6. INRIA (1992)

    Google Scholar 

  10. Felipe, E., Santana, Z., Chaves, A.P., Gerosa, M.A., Kon, F., Milojicic, D.S.: Software platforms for smart cities: concepts, requirements, challenges, and a unified reference architecture. ACM Comput. Surv. 50(6), 1–78 (2017)

    Google Scholar 

  11. Gerhart, S., Craigen, D., Ralston, T.: Case study: Paris metro signaling system. IEEE Softw. 11(1), 28–32 (1994)

    Google Scholar 

  12. Ghaemi, A.A.: A cyber-physical system approach to smart city development. In: IEEE International Conference on Smart Grid and Smart Cities (2017)

    Google Scholar 

  13. Grilo, E., Lopes, B.: Formalization and certification of software for smart cities. In: International Joint Conference on Neural Networks (IJCNN), pp. 662–669. IEEE, Piscataway (2018)

    Google Scholar 

  14. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Automata Theory, Languages, and Computation, vol. 24, International edn. Addison-Wesley, Boston (2006)

    Google Scholar 

  15. Klein, C., Kaefer, G.: From smart homes to smart cities: opportunities and challenges from an industrial perspective. In: Balandin, S., Moltchanov, D., Koucheryavy, Y. (eds.) Next Generation Teletraffic and Wired/Wireless Advanced Networking, pp. 260–260. Springer, Berlin (2008)

    Chapter  Google Scholar 

  16. Knight, J.C.: Safety critical systems: challenges and directions. In: Proceedings of the 24th International Conference on Software Engineering, pp. 547–550. ACM, New York (2002)

    Google Scholar 

  17. Kokash, N., Arbab, F.: Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems, pp. 21–41. Springer, Berlin (2009)

    Google Scholar 

  18. Lee, E.A.: Cyber physical systems: design challenges. In: 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), Orlando, 5–7 May 2008 (2008)

    Google Scholar 

  19. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: ACM SIGPLAN Notices, vol. 41, pp. 42–54. ACM, New York (2006)

    Google Scholar 

  20. Letouzey, P.: A new extraction for coq. In: International Workshop on Types for Proofs and Programs, pp. 200–219. Springer, Berlin (2002)

    Google Scholar 

  21. Leveson, N., et al.: Medical devices: The therac-25. Appendix of: Safeware: System Safety and Computers. Addison-Wesley, Boston (1995)

    Google Scholar 

  22. Leveson, N.G., Turner, C.S.: An investigation of the therac-25 accidents. IEEE Comput. 26(7), 18–41 (1993)

    Article  Google Scholar 

  23. Loveland, D.W.: Automated Theorem Proving: a Logical Basis. Elsevier, New York (2014)

    MATH  Google Scholar 

  24. Milner, R.: Some directions in concurrency theory. Futur. Gener. Comput. Syst. 88, 163–164 (1988)

    Google Scholar 

  25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Berlin (2002)

    Book  Google Scholar 

  26. Ostro, J.S.: Formal methods for the specification and design of real-time safety critical systems. J. Syst. Softw. 18(1), 33–60 (1992)

    Article  Google Scholar 

  27. Peleska, J.: Formal methods for test automation-hard real-time testing of controllers for the airbus aircraft family. In: IDPT’02, vol. 1 (2002)

    Google Scholar 

  28. Privat, G., Zhao, M., Lemke, L.: Towards a shared software infrastructure for smart homes, smart buildings and smart cities. In: International Workshop on Emerging Ideas and Trends in Engineering of Cyber-Physical Systems (2014)

    Google Scholar 

Download references

Acknowledgements

This work was partially supported by CNPq, CAPES, and FAPERJ.

Author information

Authors and Affiliations

  1. Instituto de Computação, Universidade Federal Fluminense, Niterói, Brazil

    Erick Grilo & Bruno Lopes

Authors
  1. Erick Grilo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Lopes
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Erick Grilo .

Editor information

Editors and Affiliations

  1. Institute of Computer Science, Universidade Federal Fluminense, Niterói, Rio de Janeiro, Brazil

    Vitor Nazário Coelho

  2. Instituto de Matemática e Estatística, Universidade do Estado do Rio de Janeiro, Rio de Janeiro, Rio de Janeiro, Brazil

    Igor Machado Coelho

  3. Department of Engineering and Information and Communication Technologies, Universitat Pompeu Fabra, Barcelona, Spain

    Thays A.Oliveira

  4. Institute of Computer Science, Universidade Federal Fluminense, Niterói, Rio de Janeiro, Brazil

    Luiz Satoru Ochi

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Grilo, E., Lopes, B. (2019). Critical Systems for Smart Cities: Towards Certifying Software. In: Nazário Coelho, V., Machado Coelho, I., A.Oliveira, T., Ochi, L.S. (eds) Smart and Digital Cities. Urban Computing. Springer, Cham. https://doi.org/10.1007/978-3-030-12255-3_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-12255-3_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-12254-6

  • Online ISBN: 978-3-030-12255-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation