A formal and sound transformation from Focal to UML: an application to airport security regulations | Innovations in Systems and Software Engineering Skip to main content
Springer Nature Link
Log in

A formal and sound transformation from Focal to UML: an application to airport security regulations

  • Original Paper
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

We propose an automatic transformation of Focal specifications to UML class diagrams. The main motivation for this work lies within the framework of the EDEMOI project, which aims to integrate and apply several requirements engineering and formal methods techniques to analyze airport security regulations. The idea is to provide a graphical documentation of formal models for developers, and in the long-term, for certification authorities. The transformation is formally described and an implementation has been designed. We also show how the soundness of our approach can be achieved.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bonichon R, Delahaye D, Doligez D (2007) Zenon: An extensible automated theorem prover producing checkable proofs. In: Logic for programming artificial intelligence and reasoning (LPAR). LNCS/LNAI, vol 4790. Springer, Heidelberg , pp 151–165

  2. Caron O, Carré B, Muller A, Vanwormhoudt G (2004) An OCL formulation of UML2 template binding. In: UML modeling languages and applications (UML). LNCS, vol 3273. Springer, Heidelberg, pp 27–40

  3. Delahaye D, Étienne J-F, Viguié Donzeau-Gouge V (2006) Certifying airport security regulations using the Focal environment. In: Formal methods (FM). LNCS, vol 4085. Springer, Heidelberg, pp 48–63

  4. Delahaye D, étienne J-F, Viguié Donzeau-Gouge V (2006) Reasoning about airport security regulations using the Focal environment. In: International symposium on leveraging applications of formal methods, verification and validation (ISoLA). IEEE CS Press, New York, pp 45–52

  5. Delahaye D, étienne J-F, Viguié Donzeau-Gouge V (2008) Producing UML models from Focal specifications: an application to airport security regulations. In: Theoretical aspects of software engineering (TASE). IEEE CS Press, New York

  6. Dubois C, Hardin T, Viguié Donzeau-Gouge V (2004) Building certified components within Focal. In: Trends in functional programming (TFP), vol 5. Intellect, pp 33–48

  7. Dupuy S, Ledru Y, Chabre-Peccoud M (2000) An Overview of RoZ: a tool for integrating UML and Z specifications. In: Conference on advanced information systems engineering (CAiSE). LNCS, vol 1789. Springer, Heidelberg, pp 417–430

  8. Goldschmidt T, Becker S, Uhl A (2008) Classification of concrete textual syntax mapping approaches. In: European conference on model driven architecture—foundations and applications (ECMDA-FA). LNCS, vol 5095. Springer, Heidelberg, pp 169–184

  9. Idani A, Ledru Y (2006) Dynamic graphical UML views from formal B specifications. Int J Inf Softw Technol 48(3): 154–169

    Article  Google Scholar 

  10. Jouault F, Kurtev I (2007) On the interoperability of model-to-model transformation languages. Sci Comput Program 68(3): 114–137

    Article  MATH  Google Scholar 

  11. Kim S-K, Carrington DA (2000) A formal mapping between UML models and Object-Z specifications. In: International Z and B conference (ZB). LNCS, vol 1878. Springer, Heidelberg, pp 2–21

  12. Laleau R, Polack F (2002) Coming and going from UML to B a proposal to support traceability in rigorous is development. In: International Z and B conference (ZB). LNCS, vol 2272. Springer, Heidelberg, pp 517–534

  13. Maarek M, Prevosto V (2003) FocDoc : The documentation system of Foc. In: Calculemus. LIP6

  14. The EDEMOI Project (2003). http://www-lsr.imag.fr/EDEMOI/

  15. The Focal Development Team. Focal, version 0.3.1. CNAM/INRIA/LIP6 (2005). Available at: http://focal.inria.fr/

  16. The Object Management Group (2007) Unified modeling language: superstructure, version 2.1.1. Available at: http://www.omg.org/

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, CEDRIC/CNAM, 292 rue Saint-Martin, 75141, Paris Cedex 03, France

    David Delahaye, Jean-Frédéric Étienne & Véronique Viguié Donzeau-Gouge

Authors
  1. David Delahaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Frédéric Étienne
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Véronique Viguié Donzeau-Gouge
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Delahaye.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Delahaye, D., Étienne, JF. & Viguié Donzeau-Gouge, V. A formal and sound transformation from Focal to UML: an application to airport security regulations. Innovations Syst Softw Eng 4, 267–274 (2008). https://doi.org/10.1007/s11334-008-0060-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-008-0060-5

Keywords

Search

Navigation