Skip to main content
Erschienen in: Soft Computing 15/2020

07.02.2020 | Focus

Formal modelling of OWL ontologies-based requirements for the development of safe and secure smart city systems

verfasst von: Eman Alkhammash

Erschienen in: Soft Computing | Ausgabe 15/2020

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Formal methods are mathematical techniques used for developing reliable and verified systems. Event-B formal method is proved to be very useful to construct models of systems that are corrected by construction. Developing safe, secure, and reliable smart systems is essential for effective smart city solutions. The integration of safety and security mechanisms is an important aspect to achieve trust in smart cities’ services and applications. In this paper, we present prototype for the development of smart systems using OWL ontologies and Event-B formal models. We focus on the proposed approach that uses OWL ontologies to generate Event-B formal models for secure and safe development of systems. In recent years, ontologies-driven approaches have been applied during different phases to requirements engineering (RE), such as elicitation, analysis, specification, and validation. Many empirical studies have demonstrated benefits of the application of ontologies to handle ambiguity, inconsistency and incompleteness of requirements. We derive benefit from OWL ontologies to produce textual requirements that are consistent, complete, and unambiguous for formal modelling and to manage traceability between requirements and models. The approach uses Protégé-OWL editor, OWL verbaliser, Rodin platform, and OntoGraf tool. Protégé-OWL editor enables to build and view ontologies in Web Ontology Language (OWL). OWL verbaliser is used to generate controlled English requirements called Attempto Controlled English (ACE) from OWL ontologies. ACE representation is used as input requirements and transformed into Event-B formal models. Rodin platform is used for specification, refinement and proof. OntoGraf is a tool in Protégé that is used to visualise ontologies, and we make use of OntoGraf in this paper to assist in deciding refinement strategy and managing traceability between requirements and models.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Literatur
Zurück zum Zitat Abrial J (2010) Modeling in Event-B—system and software engineering. Cambridge University Press, CambridgeCrossRef Abrial J (2010) Modeling in Event-B—system and software engineering. Cambridge University Press, CambridgeCrossRef
Zurück zum Zitat Abrial J, Butler M, Hallerstede S, Hoang T, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6):447–466CrossRef Abrial J, Butler M, Hallerstede S, Hoang T, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6):447–466CrossRef
Zurück zum Zitat Alkhammash EH (2016) Derivation of Event-B models from OWL ontologies. In: MATEC web of conferences, EDP Sciences 04008, Vol 76 Alkhammash EH (2016) Derivation of Event-B models from OWL ontologies. In: MATEC web of conferences, EDP Sciences 04008, Vol 76
Zurück zum Zitat Alkhammash E, Butler M, Salehi A, Cristea C (2015) Building traceable Event-B models from requirements. Sci Comput Program 111(part2):318–338 Special issue on automated verification of critical systems (AVoCS 2013)CrossRef Alkhammash E, Butler M, Salehi A, Cristea C (2015) Building traceable Event-B models from requirements. Sci Comput Program 111(part2):318–338 Special issue on automated verification of critical systems (AVoCS 2013)CrossRef
Zurück zum Zitat Arqub OA (2017) Adaptation of reproducing kernel algorithm for solving fuzzy Fredholm–Volterra integrodifferential equations. Neural Comput Appl 28(7):1591–1610CrossRef Arqub OA (2017) Adaptation of reproducing kernel algorithm for solving fuzzy Fredholm–Volterra integrodifferential equations. Neural Comput Appl 28(7):1591–1610CrossRef
Zurück zum Zitat Arqub OA, Abo-Hammour Z (2014) Numerical solution of systems of second-order boundary value problems using continuous genetic algorithm. Inf Sci 279:396–415MathSciNetCrossRef Arqub OA, Abo-Hammour Z (2014) Numerical solution of systems of second-order boundary value problems using continuous genetic algorithm. Inf Sci 279:396–415MathSciNetCrossRef
Zurück zum Zitat Arqub OA, Mohammed AS, Momani S, Hayat T (2016) Numerical solutions of fuzzy differential equations using reproducing kernel Hilbert space method. Soft Comput 20(8):3283–3302CrossRef Arqub OA, Mohammed AS, Momani S, Hayat T (2016) Numerical solutions of fuzzy differential equations using reproducing kernel Hilbert space method. Soft Comput 20(8):3283–3302CrossRef
Zurück zum Zitat Arqub OA, Al-Smadi M, Momani S, Hayat T (2017) Application of reproducing kernel algorithm for solving second-order, two-point fuzzy boundary value problems. Soft Comput 21(23):7191–7206CrossRef Arqub OA, Al-Smadi M, Momani S, Hayat T (2017) Application of reproducing kernel algorithm for solving second-order, two-point fuzzy boundary value problems. Soft Comput 21(23):7191–7206CrossRef
Zurück zum Zitat Avdeenko T, Pustovalova N (2015) The ontology-based approach to support the completeness and consistency of the requirements specification. In: Control and communications (SIBCON), 2015 international siberian conference on, pp 1–4 Avdeenko T, Pustovalova N (2015) The ontology-based approach to support the completeness and consistency of the requirements specification. In: Control and communications (SIBCON), 2015 international siberian conference on, pp 1–4
Zurück zum Zitat Bartoli A, Hernández-Serrano J, Soriano M, Dohler M, Kountouris A, Barthel D (2011) Security and privacy in your smart city. Proc Barc Smart Cities Congr 292:1–6 Bartoli A, Hernández-Serrano J, Soriano M, Dohler M, Kountouris A, Barthel D (2011) Security and privacy in your smart city. Proc Barc Smart Cities Congr 292:1–6
Zurück zum Zitat Belanche-Gracia D, Casaló-Ariño LV, Pérez-Rueda A (2015) Determinants of multi-service smartcard success for smart cities development: a study based on citizens privacy and security perceptions. Gov Inf Q 32(2):154–163CrossRef Belanche-Gracia D, Casaló-Ariño LV, Pérez-Rueda A (2015) Determinants of multi-service smartcard success for smart cities development: a study based on citizens privacy and security perceptions. Gov Inf Q 32(2):154–163CrossRef
Zurück zum Zitat Belgueliel Y, Bourahla M, Brik M (2014) Towards an ontology for UML state machines. Lect Notes Softw Eng 2(1):116–120CrossRef Belgueliel Y, Bourahla M, Brik M (2014) Towards an ontology for UML state machines. Lect Notes Softw Eng 2(1):116–120CrossRef
Zurück zum Zitat Borst WN (1997) Construction of engineering ontologies for knowledge sharing and reuse. Enschede, The Netherlands Borst WN (1997) Construction of engineering ontologies for knowledge sharing and reuse. Enschede, The Netherlands
Zurück zum Zitat Castaneda V, Ballejos L, Caliusco L, Galli MR (2010) The use of ontologies in requirements engineering. Glob J Res Eng specif 10(6):2–8 Castaneda V, Ballejos L, Caliusco L, Galli MR (2010) The use of ontologies in requirements engineering. Glob J Res Eng specif 10(6):2–8
Zurück zum Zitat Cerón R, Dueñas JC, Serrano E, Capilla R (2005) A Meta-model for requirements engineering in system family context for software process improvement using CMMI. Springer, BerlinCrossRef Cerón R, Dueñas JC, Serrano E, Capilla R (2005) A Meta-model for requirements engineering in system family context for software process improvement using CMMI. Springer, BerlinCrossRef
Zurück zum Zitat Chetali B, Nguyen QH (2008) Industrial use of formal methods for a high-level security evaluation. In: international symposium on formal methods, Springer, Switzerland, pp 198–213 Chetali B, Nguyen QH (2008) Industrial use of formal methods for a high-level security evaluation. In: international symposium on formal methods, Springer, Switzerland, pp 198–213
Zurück zum Zitat Cui L, Xie G, Qu Y, Gao L, Yang Y (2018) Security and privacy in smart cities: challenges and opportunities. IEEE access 6:46134–46145CrossRef Cui L, Xie G, Qu Y, Gao L, Yang Y (2018) Security and privacy in smart cities: challenges and opportunities. IEEE access 6:46134–46145CrossRef
Zurück zum Zitat Dermeval D, Vilela J, Bittencourt II, Castro J, Isotani S, Brito P, Silva A (2015) Application of ontologies in requirements engineering: a systematic review of the literature. Requir Eng 21:1–33 Dermeval D, Vilela J, Bittencourt II, Castro J, Isotani S, Brito P, Silva A (2015) Application of ontologies in requirements engineering: a systematic review of the literature. Requir Eng 21:1–33
Zurück zum Zitat Dermeval D, Vilela J, Bittencourt II, Castro J, Isotani S, Brito P (2014) A systematic review on the use of ontologies in requirements engineering. In: Software engineering (SBES), 2014 brazilian symposium on, pp 1–10 Dermeval D, Vilela J, Bittencourt II, Castro J, Isotani S, Brito P (2014) A systematic review on the use of ontologies in requirements engineering. In: Software engineering (SBES), 2014 brazilian symposium on, pp 1–10
Zurück zum Zitat Elmaghraby AS, Losavio MM (2014) Cyber security challenges in smart cities: safety, security and privacy. J Adv Res 5(4):491–497CrossRef Elmaghraby AS, Losavio MM (2014) Cyber security challenges in smart cities: safety, security and privacy. J Adv Res 5(4):491–497CrossRef
Zurück zum Zitat Fitzgerald J, Bicarregui J, Larsen PG, Woodcock J (2013) Industrial deployment of formal methods: trends and challenges. Industrial Deployment of System Engineering Methods. Springer, Heidelberg, pp 123–143CrossRef Fitzgerald J, Bicarregui J, Larsen PG, Woodcock J (2013) Industrial deployment of formal methods: trends and challenges. Industrial Deployment of System Engineering Methods. Springer, Heidelberg, pp 123–143CrossRef
Zurück zum Zitat Fuchs N, Kaljur K, Schneider G (2006) Attempto controlled English meets the challenges of knowledge representation, reasoning, interoperability and user interfaces. In: Proceedings of 19th international Florida artificial intelligence research society conference, vol 12, pp 664–669 Fuchs N, Kaljur K, Schneider G (2006) Attempto controlled English meets the challenges of knowledge representation, reasoning, interoperability and user interfaces. In: Proceedings of 19th international Florida artificial intelligence research society conference, vol 12, pp 664–669
Zurück zum Zitat Hallerstede E, Jastram M, Ladenberger L (2014) A method and tool for tracing requirements into specifications. Sci Comput Program 82:2–21 Special issue on automated verification of critical systems (AVoCS 2013)CrossRef Hallerstede E, Jastram M, Ladenberger L (2014) A method and tool for tracing requirements into specifications. Sci Comput Program 82:2–21 Special issue on automated verification of critical systems (AVoCS 2013)CrossRef
Zurück zum Zitat Harith A (2003) Tgviztab: an ontology visualisation extension for protégé. In: Knowledge capture (K-Cap’03), workshop on visualization information in knowledge engineering Harith A (2003) Tgviztab: an ontology visualisation extension for protégé. In: Knowledge capture (K-Cap’03), workshop on visualization information in knowledge engineering
Zurück zum Zitat Haxthausen AE (2011) Towards a framework for modelling and verification of relay interlocking systems. In: Calinescu R, Jackson E (eds) Foundations of computer software. Modeling, development, and verification of adaptive systems. Monterey Workshop (2010) Lecture Notes in Computer Science, vol 6662. Springer, Berlin, Heidelberg Haxthausen AE (2011) Towards a framework for modelling and verification of relay interlocking systems. In: Calinescu R, Jackson E (eds) Foundations of computer software. Modeling, development, and verification of adaptive systems. Monterey Workshop (2010) Lecture Notes in Computer Science, vol 6662. Springer, Berlin, Heidelberg
Zurück zum Zitat Heflin J (2007) An introduction to the OWL web ontology language. Lehigh University, National Science Foundation (NSF) Heflin J (2007) An introduction to the OWL web ontology language. Lehigh University, National Science Foundation (NSF)
Zurück zum Zitat Horridge M, Knublauch H, Rector A, Stevens R, Wroe C (2004) A practical guide to building OWL ontologies using the Protégé-OWL plugin and CO-ODE tools edition 1.0. University of Manchester Horridge M, Knublauch H, Rector A, Stevens R, Wroe C (2004) A practical guide to building OWL ontologies using the Protégé-OWL plugin and CO-ODE tools edition 1.0. University of Manchester
Zurück zum Zitat Kaljur K, Fuchs N (2007) Verbalizing owl in attempto controlled english. In: Proceedings of OWLED07, vol 258 Kaljur K, Fuchs N (2007) Verbalizing owl in attempto controlled english. In: Proceedings of OWLED07, vol 258
Zurück zum Zitat Kroha P, Janetzko R, Labra JE (2009) Ontologies in checking for inconsistency of requirements specification. In: Proceedings of the 2009 third international conference on advances in semantic processing. SEMAPRO ’09, Washington, IEEE computer society, pp 32–37 Kroha P, Janetzko R, Labra JE (2009) Ontologies in checking for inconsistency of requirements specification. In: Proceedings of the 2009 third international conference on advances in semantic processing. SEMAPRO ’09, Washington, IEEE computer society, pp 32–37
Zurück zum Zitat Siegemund K, Thomas EJ, Zhao Y, Pan J, Assmann U (2011)Towards ontology-driven requirements engineering. In: Workshop semantic web enabled software engineering at 10th international semantic web conference (ISWC), Bonn Siegemund K, Thomas EJ, Zhao Y, Pan J, Assmann U (2011)Towards ontology-driven requirements engineering. In: Workshop semantic web enabled software engineering at 10th international semantic web conference (ISWC), Bonn
Zurück zum Zitat Sirin E, Parsia B, Grau BC, Kalyanpur A, Katz Y (2007) Pellet: A practical OWL–DL reasoner. Web Semant 5(2):51–53CrossRef Sirin E, Parsia B, Grau BC, Kalyanpur A, Katz Y (2007) Pellet: A practical OWL–DL reasoner. Web Semant 5(2):51–53CrossRef
Zurück zum Zitat Sommerville I, Sawyer P (1997) Requirements engineering: a good practice guide, 1st edn. John Wiley & Sons Inc, New YorkMATH Sommerville I, Sawyer P (1997) Requirements engineering: a good practice guide, 1st edn. John Wiley & Sons Inc, New YorkMATH
Zurück zum Zitat Su K, Li J, Fu H (2011) Smart city and the applications. In: 2011 international conference on electronics, communications and control (ICECC), IEEE pp 1028–1031 Su K, Li J, Fu H (2011) Smart city and the applications. In: 2011 international conference on electronics, communications and control (ICECC), IEEE pp 1028–1031
Zurück zum Zitat Thayer RH, Bailin SC, Dorfman M (1997) Software requirements engineerings, 2nd edn. IEEE Computer Society Press, Los Alamitos Thayer RH, Bailin SC, Dorfman M (1997) Software requirements engineerings, 2nd edn. IEEE Computer Society Press, Los Alamitos
Zurück zum Zitat Thomas M (1993) The industrial use of formal methods. Microprocess Microsyst 17(1):31–36CrossRef Thomas M (1993) The industrial use of formal methods. Microprocess Microsyst 17(1):31–36CrossRef
Zurück zum Zitat Van Zoonen L (2016) Privacy concerns in smart cities. Gov Inf Q 33(3):472–480CrossRef Van Zoonen L (2016) Privacy concerns in smart cities. Gov Inf Q 33(3):472–480CrossRef
Zurück zum Zitat Weinberg G (1997) Quality software management: anticipating change. Dorset House, Oxford Weinberg G (1997) Quality software management: anticipating change. Dorset House, Oxford
Zurück zum Zitat Yeganefard S, Butler M (2012) Control systems: phenomena and structuring functional requirement documents. In: engineering of complex computer systems (ICECCS), 2012 17th international conference on, pp 39–48 Yeganefard S, Butler M (2012) Control systems: phenomena and structuring functional requirement documents. In: engineering of complex computer systems (ICECCS), 2012 17th international conference on, pp 39–48
Zurück zum Zitat Zhang K, Ni J, Yang K, Liang X, Ren J, Shen XS (2017) Security and privacy in smart city applications: challenges and solutions. IEEE Commun Mag 55(1):122–129CrossRef Zhang K, Ni J, Yang K, Liang X, Ren J, Shen XS (2017) Security and privacy in smart city applications: challenges and solutions. IEEE Commun Mag 55(1):122–129CrossRef
Metadaten
Titel
Formal modelling of OWL ontologies-based requirements for the development of safe and secure smart city systems
verfasst von
Eman Alkhammash
Publikationsdatum
07.02.2020
Verlag
Springer Berlin Heidelberg
Erschienen in
Soft Computing / Ausgabe 15/2020
Print ISSN: 1432-7643
Elektronische ISSN: 1433-7479
DOI
https://doi.org/10.1007/s00500-020-04688-z

Weitere Artikel der Ausgabe 15/2020

Soft Computing 15/2020 Zur Ausgabe