A maintainable and iterative development approach of critical systems with FoCaLiZe

Authors

  • Fatima Haloua
  • Messaoud Abbas
  • Ammar Boucherit
  • Hessa Alfraihi

DOI:

https://doi.org/10.54021/seesv5n1-092

Keywords:

software engineering, development lifecycles, model verification, formal methods, UML/OCL, FoCaLiZe

Abstract

The life-cycle development of critical systems follows mainly a V-cycle process overlapped with proofs and/or verification techniques. At the first development stage, a critical system must be, precisely, and as completely as possible described. Thus, it is recommended to use a graphical modeling language standard such as the Unified Modeling Language (UML) and the Object Constraint Language (OCL), to which both customers and developers could contribute. Then, the graphical design with its formal specification (requirements) is mapped into a complete formal development environment, using an MDE (Model-driven engineering) approach. The formal environment has to assess the development until the generation of a secure code. In this context, we propose a life-cycle development approach that combines UML/OCL and the FoCaLiZe formal environment for the secure development of critical systems. The proposed approach ensures essential development constraints such as strict boundaries and traceability between development phases. It also ensures a secure maintenance phase using partial transformation techniques from UML/OCL to FoCaLiZe. The latter enhances the transformation from UML/OCL into FoCaLiZe to support incremental development and assist developers in correcting modeling errors. The proposed approach is mostly dedicated to secure and maintainable lifecycle development processes of critical systems. The formal environment assesses the development process until the generation of a secure code. To illustrate the proposed approach, we present the stages of development of a constrained system controlling military objects. The development of this system uses the iterative, incremental, and maintainability stages as described by the development approach, until the generation of secure code.

References

ABBAS, M.; BEN-YELLES, C. B.; RIOBOO, R. Formalizing UML/OCL multiple inheritance with FoCaLiZe. In: Proceedings of the 2018 International Conference on Smart Communications in Network Technologies (SaCoNeT). IEEE, 2018. p. 261–266.

ABBAS, M.; BEN-YELLES, C. B.; RIOBOO, R. Formalizing UML/OCL structural features with FoCaLiZe. Soft Computing, v. 24, p. 4149–4164, 2020.

ABBAS, M.; BEN-YELLES, C. B.; RIOBOO, R. Modeling UML template classes with FoCaLiZe. In: Proceedings of the International Conference on Integrated Formal Methods. Springer, 2014.

ABBAS, M.; BEN-YELLES, C. B.; RIOBOO, R. Modelling UML state machines with FoCaLiZe. International Journal of Information and Communication Technology, v. 13, p. 34–54, 2018.

ABBAS, M.; HALOUA, F.; BOUCHERIT, A. Development of Critical Systems with UML/OCL and FoCaLiZe. In: Proceedings of the International Conference on Model and Data Engineering. Springer, 2021. p. 16–30.

ABBAS, M.; RIOBOO, R.; BEN-YELLES, C. B.; SNOOK, C. F. Formal modeling and verification of UML Activity Diagrams (UAD) with FoCaLiZe. Journal of Systems Architecture, v. 114, p. 101911, 2021.

ABRIAL, J. R. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.

ABRIAL, J. R. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 2005.

ANASTASAKIS, K.; BORDBAR, B.; GEORG, G.; RAY, I. UML2Alloy: A Challenging Model Transformation. In: Model Driven Engineering Languages and Systems. Springer, 2007. p. 436–450.

ANWAR, A. A review of rup (rational unified process). International Journal of Software Engineering (IJSE), v. 5, p.12–19, 2014.

AYRAULT, P.; HARDIN, T.; PESSAUX, F. Development Life-Cycle of Critical Software under FoCal. Electronic Notes in Theoretical Computer Science, v. 243, p. 15–31, 2009.

BENEDICENTI, L.; MESSINA, A.; SILLITTI, A. iAgile: mission critical military software development. In: Proceedings of the 2017 International Conference on High Performance Computing & Simulation (HPCS). IEEE, 2017. p. 545–552.

BENMAN, E.; AIMEN, D. Toward the Development of a Unified Process and Methodology Guide for Environmental Justice Analysis in Planning and Programming. Transportation Research Record, p. 03611981211028868, 2021.

BONICHON, R.; DELAHAYE, D.; DOLIGEZ, D. Zenon: An extensible automated theorem prover producing checkable proofs. In: Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 2007. p. 151–165.

BONICHON, R.; DELAHAYE, D.; DOLIGEZ, D. Zenon: An extensible automated theorem prover producing checkable proofs. In: Proceedings of the LPAR. Springer, 2007. v. 4790, p. 151–165.

BOUHAMED, M.M.; CHAOUI, A.; NOUARA, R.; DÍAZ, G.; DEMBRI, A. Reducing the number of migrated instances during business process change: A graph rewriting approach. Journal of King Saud University-Computer and Information Sciences, v. 34, p. 7720–7734, 2022.

BOUHAMED, M. M.; DÍAZ, G.; CHAOUI, A.; KAMEL, O.; NOUARA, R. Models@ Runtime: The Development and Re-Configuration Management of Python Applications Using Formal Methods. Applied Sciences, v. 11, p. 9743, 2021.

BOUZENADA, A.; BOUHAMED, M. M.; KAMEL, O.; MACIÀ, H.; DÍAZ, G.; CHAOUI, A. An Example of a Dynamic CPN Model to Obtain Routes in the Presence of Obstacles Detected Using Machine Learning Techniques. In: Proceedings of the International Symposium on Modelling and Implementation of Complex Systems. Springer, 2023. p. 220–233.

BROWN, S. Overview of IEC 61508. Design of electrical/ electronic/ programmable electronic safety-related systems. Computing & Control Engineering Journal, v. 11, p. 6–12, 2000.

BROY, M.; CRANE, M.; DINGEL, J.; HARTMAN, A.; RUMPE, B.; SELIC, B. Formal Semantics for UML. Models in Software Engineering, 2007. p. 318–323.

BRUCKER, A. D.; WOLFF, B. HOL-OCL: A Formal Proof Environment for UML/OCL. In: Fundamental Approaches to Software Engineering. Springer, 2008. p. 97–100.

CABOT, J.; PAU, R.; RAVENTÓS, R. From UML/OCL to SBVR specifications: A challenging transformation. Information systems, v. 35, p. 417–440, 2010.

CARLIER, M.; DUBOIS, C. Functional testing in the focal environment. In: Proceedings of the International Conference on Tests and Proofs. Springer, 2008. p. 84–98.

CHABBAT, N.; SAIDOUNI, D.E.; BOUKHARROU, R.; GHANEMI, S. Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model. Computing and Informatics, v. 39, p. 1022–1060, 2020.

CLAVEL, M.; DURAN, F.; EKER, S.; LINCOLN, P.; MARTI-OLIET, N.; MESEGUER, J.; QUESADA, J. F. The Maude system. In: Proceedings of the International Conference on Rewriting Techniques and Applications. Springer, 1999. p. 240–243.

CLAVEL, M.; DURÁN, F.; EKER, S.; LINCOLN, P.; MARTÍ-OLIET, N.; MESEGUER, J.; TALCOTT, C. All about Maude a High Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, 2007.

COQ. The Coq Proof Assistant, Tutorial and Reference Manual, Version 8.4. INRIA – LIP – LRI – LIX – PPS 2012. Distribution available at: http://coq.inria.fr/.

CUCCURU, A.; RADERMACHER, A.; GÉRARD, S.; TERRIER, F. Constraining Type Parameters of UML 2 Templates with Substitutable Classifiers. In: Model Driven Engineering Languages and Systems. Springer, 2009. p. 644–649.

CUNHA, A.; GARIS, A.; RIESCO, D. Translating between Alloy Specifications and UML Class Diagrams Annotated with OCL Constraints. Software & Systems Modeling, p. 1–21, 2013.

DE SOUSA, T. C.; KELVIN, L.; NETO, C. D.; DE CARVALHO, C. G. N. A Formal Semantics for Use Case Diagram Via Event-B. J. Softw., v. 12, p. 189–200, 2017.

DE-LA HOZ-HERNÁNDEZ, J. D.; TRONCOSO-PALACIO, A.; DE-LA HOZ-FRANCO, E. Implementation of the Eclipse Process Framework Composer Tool for the Documentation of Quality Management Systems: A Case Applied in Healthcare Services. In: Proceedings of the International Conference on Swarm Intelligence. Springer, 2019. p. 200–210.

DELAHAYE, D.; ÉTIENNE, J.; DONZEAU-GOUGE, V. Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. In: Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008. p. 121–124.

DELAHAYE, D.; ÉTIENNE, J.; DONZEAU-GOUGE, V. Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. In: Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008. p. 121–124.

DGHAYM, D.; POPPLETON, M.; SNOOK, C. Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3. In: Proceedings of the International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Springer, 2018. p. 338–352.

DJAOUI, C.; KERKOUCHE, E.; CHAOUI, A.; KHALFAOUI, K. A Graph Transformation Approach to Generate Analysable Maude Specifications from UML Interaction Overview Diagrams. In: Proceedings of the 2018 IEEE International Conference on Information Reuse and Integration (IRI). IEEE, 2018. p. 511–517.

DOLIGEZ, D.; JAUME, M.; RIOBOO, R. Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment. In: Proceedings of the Proceedings of the 7th Workshop on Programming Languages and Analysis for Security, 2012. p. 1–12

DUBOIS, C.; HARDIN, T.; DONZEAU-GOUGE, V. Building Certified Components within FOCAL. Trends in Functional Programming, v. 5, p. 33–48, 2006.

DURÁN, F.; GOGOLLA, M.; ROLDÁN, M. Tracing Properties of UML and OCL Models with Maude.arXiv preprint arXiv: 1107.0068 2011.

EDEKI, C. Agile unified process. International Journal of Computer Science, v. 1, p. 13–17, 2013.

ESCHBACH, R. Industrial application of Event-B to a wayside train monitoring system: Formal conceptual data analysis. In: Proceedings of the International Symposium on Formal Methods. Springer, 2019. p. 738–745.

FACON, P.; LALEAU, R. Des spécifications informelles aux spécifications formelles : compilation ou interprétation? Actes du 13ème congrès INFORSID, 1995.

FECHTER, S. Sémantique des Traits Orientés Objet de Focal. Thesis (Doctorate) – Paris 6, 2005.

FRANÇOIS, P. Another Tutorial for FoCaLize: Playing with Proofs. 2013.

GU, J.; CHEN, M.; X., Z. Formal Language B and UML/OCL Comparison. Computer Knowledge and Technology, v. 34, 2009.

HADAD, A. S. A.; MA, C.; AHMED, A. A. O. Formal Verification of AADL Models by Event-B. IEEE Access, v. 8, p. 72814–72834, 2020.

HARDIN, T.; FRANCOIS, P.; PIERRE, W.; DAMIEN, D. FoCaLiZe: Tutorial and Reference Manual, version 0.9.2. CNAM/INRIA/LIP6 2018. available at: http://focalize.inria.fr.

HAZEM, L.; LEVY, N.; MARCANO-KAMENOFF, R. UML2B: Un Outil pour la Génération de Modèle Formels. In: Proceedings of the AFADL, 2004.

HE, X. PZ nets—a formal method integrating Petri nets with Z. Information and Software Technology, v. 43, p. 1–18, 2001.

INFRASTRUCTURE, P. K.; PROfiLE, T. P. Common criteria for information technology security evaluation. National Security Agency 2002.

JACKSON, D. Software Abstractions: Logic, Language and Anlysis; MIT press, 2012.

JACKSON, D. Software Abstractions: logic, language, and analysis; MIT press. Cambridge: Great Britain, 2012.

KAUTZ, O.; MAOZ, S.; RINGERT, J. O.; RUMPE, B. CD2Alloy: a translation of class diagrams to Alloy. Techn. Rep. AIB-2017-06, RWTH Aachen University (July 2017) 2017.

KHERBOUCHE, M.; MOLNÁR, B. Formal Model Checking and Transformations of Models Represented in UML with Alloy. In: Proceedings of the International Workshop on Modelling to Program. Springer, 2020. p. 127–136.

KIENZLE, J.; AL ABED, W.; FLEUREY, F.; JÉZÉQUEL, J. M.; KLEIN, J. Aspect-oriented Design with Reusable Aspect Models. In: Transactions on aspect-oriented software development VII. Springer, 2010. p. 272–320.

KRAIBI, K.; AYED, R.B.; COLLART-DUTILLEUL, S.; BON, P.; PETIT, D. Analysis and Formal Modeling of Systems Behavior Using UML/Event-B. Journal of Communications, v. 14, p. 980–986, 2019.

LEDANG, H.; SOUQUIÈRES, J.; CHARLES, S. et al. ArgoUML+ B: Un Outil de Transformation Systématique de Spécifications UML en B. In: Proceedings of the Approches Formelles dans l’Assistance au Développement de Logiciels, 2003.

MITHUN, P.; SAMUEL, A.A.; RANJAN, P.; JAYALAL, N.; GOPALAKRISHNAN, T.; VALSA, B. A Framework for Test Coverage of Safety and Mission Critical Software. In: Proceedings of the Second International Conference on Networks and Advances in Computational Technologies. Springer, 2021. p. 37–47.

MOKHATI, F.; SAHRAOUI, B.; BOUZAHER, S.; KIMOUR, M. T. A Tool for Specifying and Validating Agents’ Interaction Protocols: From Agent UML to Maude. Object Technology 2010, 9.

MUHAMAD, Z. H.; ABDULMONIM, D. A.; ALATHARI, B. An integration of uml use case diagram and activity diagram with Z language for formalization of library management system. International Journal of Electrical and Computer Engineering, v. 9, p. 3069, 2019.

NIPKOW, T.; PAULSON, L. Isabelle HOL-the tutorial 2001.

NIPKOW, T.; PAULSON, L. C.; WENZEL, M. Isabelle/HOL: A Proof Assistant for Higher-order Logic; Springer, 2002. v. 2283.

NOULAMO, T.; TANYI, E.; NKENLIFACK, M.; LIENOU, J. P.; DJIMELI, A. Formalization Method of the UML Statechart by Transformation Toward Petri Nets. IAENG International Journal of Computer Science, v. 45, 2018.

O’REGAN, G. Z formal specification language. In: Concise Guide to Formal Methods. Springer, 2017. p. 155–171.

OMG. OCL: Object Constraint Language 2.4 2018. available at: https://www.omg.org/spec/OCL/2.4/PDF.

OMG. UML: Unified Modeling Language, version 2.5, 2017. available at:https://www.omg.org/spec/UML/2.5.1/PDF.

OMG. XML Metadata Interchange (XMI) Specification 2.5.1 2015. Available at: https://www. omg.org/spec/XMI/2.5.1/PDF.

OUESLATI, R.; MOSBAHI, O.; KHALGUI, M.; LI, Z.; QU, T. Combining semi-formal and formal methods for the development of distributed reconfigurable control systems. IEEE Access, v. 6, p. 70426–70443, 2018.

RIOBOO, R. Invariants for the FoCaL Language. Annals of Mathematics and Artificial Intelligence, v. 56, p. 273–296, 2009.

SINGH, N. K.; LAWFORD, M.; MAIBAUM, T. S.; WASSYNG, A. A formal approach to rigorous development of critical systems. Journal of Software: Evolution and Process, p. e2334, 2021.

SNOOK, C.; BUTLER, M. UML-B: Formal Modeling and Design Aided by UML. ACM Transactions on Software Engineering and Methodology (TOSEM), v. 15, p. 92–122, 2006.

SNOOK, C.; SAVICKS, V.; BUTLER, M. Verification of UML Models by Translation to UML-B. In: Proceedings of the Formal Methods for Components and Objects. Springer, 2012. p. 251–266.

SUNYÉ, G.; LE GUENNEC, A.; JÉZÉQUEL, J. M. Design Patterns Application in UML. In: ECOOP 2000—Object-Oriented Programming. Springer, 2000. p. 44–62.

UNHELKAR, B. Software Engineering with UML. CRC Press, 2017.

WAKRIME, A. A.; AYED, R. B.; COLLART-DUTILLEUL, S.; LEDRU, Y.; IDANI, A. Formalizing railway signaling system ERTMS/ETCS using UML/Event-B. In:. Proceedings of the International Conference on Model and Data Engineering Springer, 2018. p. 321–330.

YANG, J. A framework for formalizing UML models with formal language rCOS. In: Proceedings of the Frontier of Computer Science and Technology, 2009. FCST’09. Fourth International Conference on. IEEE, 2009. p. 408–416.

YANG, M.; Michaelson, G.; Pooley, R. Formal Action Semantics for a UML Action Language. Journal of Universal Computer Science, v. 14, p. 3608–3624, 2008.

Downloads

Published

2024-05-15

How to Cite

Haloua, F., Abbas, M., Boucherit, A., & Alfraihi, H. (2024). A maintainable and iterative development approach of critical systems with FoCaLiZe. STUDIES IN ENGINEERING AND EXACT SCIENCES, 5(1), 1821–1871. https://doi.org/10.54021/seesv5n1-092