{"id":3524,"date":"2022-04-13T17:28:54","date_gmt":"2022-04-13T15:28:54","guid":{"rendered":"https:\/\/samovar2022.int-evry.fr\/index.php\/acmes-2\/amel-mammar-2\/"},"modified":"2022-04-13T17:29:11","modified_gmt":"2022-04-13T15:29:11","slug":"amel-mammar-2","status":"publish","type":"page","link":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/acmes-2\/amel-mammar-2\/","title":{"rendered":"Amel MAMMAR"},"content":{"rendered":"<p><div class=\"bandeau-personnel MonLaboUser\"><img decoding=\"async\" src=\"https:\/\/samovar.telecom-sudparis.eu\/wp-content\/uploads\/2022\/07\/Amel-MAMMAR.jpg\" class=\"wp-image-6 alignleft img-arrondi wp-post-image\" height=\"150\" width=\"150\" alt=\" \" \/><div class=\"adresse\"><p>SAMOVAR - SAMOVAR<br \/>Telecom SudParis<br \/>\r\n9 rue Charles Fourier<br \/>\r\n91011 EVRY CEDEX<\/p><p>Fax : +33 (0) 1 60 76 20 80<\/p><\/div><div class=\"monlaboBlocTexte\"><h1>Pr. Amel <span class=\"MonLabo-lastname\">MAMMAR<\/span><\/h1><div class=\"coordonnees\"><em>Professeur<\/em><br \/><span class=\"team-description\"><a href=\"https:\/\/samovar.telecom-sudparis.eu\/?page_id=2438\" class=\"MonLaboLink\"><span class=\"MonLabo_team_name\">ACMES<\/span><\/a><\/span><\/div><div class=\"coordonnees\"><span class=\"MonLabo-email\">amel.mammar[&#64;<span>-Code to remove to avoid SPAM-<\/span>]telecom-sudparis.eu<\/span><\/div><\/div><\/div>\n<div id=\"res_script\">\n<p class='Rubrique'>Article dans une revue<\/p>\n<p class='SousRubrique'>2024<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, R\u00e9gine Laleau. An Event-B model of an automotive adaptive exterior light system. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2024, 26, pp.331-346. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10009-024-00748-z\">&#x27E8;10.1007\/s10009-024-00748-z&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04849822v1\">&#x27E8;hal-04849822&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04849822\/file\/STTT_ABZ2020.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04849822\/file\/STTT_ABZ2020.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04849822\/file\/STTT_ABZ2020.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04849822v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Michael Leuschel. Modeling and verifying an arrival manager using the formal Event-B method. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2024. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04855142v1\">&#x27E8;hal-04855142&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04855142\/file\/STTT_ABZ2023_2024.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04855142\/file\/STTT_ABZ2023_2024.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04855142\/file\/STTT_ABZ2023_2024.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04855142v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier. Modeling of a speed control system using Event-B. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2024, 26, pp.347-363. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10009-024-00749-y\">&#x27E8;10.1007\/s10009-024-00749-y&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04849841v1\">&#x27E8;hal-04849841&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04849841\/file\/STTT_ABZ2020_CSS.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04849841\/file\/STTT_ABZ2020_CSS.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04849841\/file\/STTT_ABZ2020_CSS.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04849841v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Meriem Belguidoum, Saddam Hocine. A Formal approach for the correct deployment of cloud applications. <i>Science of Computer Programming<\/i>, 2024, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.scico.2023.103048\">&#x27E8;10.1016\/j.scico.2023.103048&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04344435v1\">&#x27E8;hal-04344435&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04344435\/file\/SCP_CouldServices.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04344435\/file\/SCP_CouldServices.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04344435\/file\/SCP_CouldServices.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04344435v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2022<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Imed Abbassi, Amel Mammar, Mohamed Graiet. A Correct-by-construction model for verifying transactional composite services configuration. <i>IEEE Transactions on Services Computing<\/i>, 2022, 15 (5), pp.2511 - 2525. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/TSC.2021.3072327\">&#x27E8;10.1109\/TSC.2021.3072327&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-03545911v1\">&#x27E8;hal-03545911&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-03545911v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Meryem Afendi, R\u00e9gine Laleau. Modeling and proving hybrid programs with event-B: an approach by generalization and instantiation. <i>Science of Computer Programming<\/i>, 2022, 222 (102856), <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.scico.2022.102856\">&#x27E8;10.1016\/j.scico.2022.102856&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/ip-paris.hal.science\/hal-03916799v1\">&#x27E8;hal-03916799&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/ip-paris.hal.science\/hal-03916799v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2021<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Lazhar Hamel, Mohamed Graiet. An Event-B-based approach to model and verify behaviors for component-based applications. <i>The Computer Journal<\/i>, 2021, 65 (10), pp.2780-2800. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1093\/comjnl\/bxab115\">&#x27E8;10.1093\/comjnl\/bxab115&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-03545928v1\">&#x27E8;hal-03545928&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-03545928v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2020<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, Marc Frappier, R\u00e9gine Laleau, Amel Mammar. Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2020, 22 (3), pp.349-363. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10009-019-00542-2\">&#x27E8;10.1007\/s10009-019-00542-2&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02975778v1\">&#x27E8;hal-02975778&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02975778v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, R\u00e9gine Laleau. A formal refinement-based analysis of the hybrid ERTMS\/ETCS level 3 standard. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2020, 22 (3), pp.333-347. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10009-019-00543-1\">&#x27E8;10.1007\/s10009-019-00543-1&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02975774v1\">&#x27E8;hal-02975774&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02975774v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2019<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nina Huynh, Marc Frappier, Herman Pooda, Amel Mammar, R\u00e9gine Laleau. SGAC: a multi-layered access control model with conflict resolution strategy. <i>The Computer Journal<\/i>, 2019, 62 (12), pp.1707-1733. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1093\/comjnl\/bxz039\">&#x27E8;10.1093\/comjnl\/bxz039&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02403976v1\">&#x27E8;hal-02403976&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02403976v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Jlassi Sindyana, Amel Mammar, Imed Abbassi, Mohamed Graiet. Towards correct cloud resource allocation in FOSS applications. <i>Future Generation Computer Systems<\/i>, 2019, 91 (392-406), <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.future.2018.08.030\">&#x27E8;10.1016\/j.future.2018.08.030&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02403919v1\">&#x27E8;hal-02403919&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02403919v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Lionel Tidjon, Marc Frappier, Amel Mammar. Intrusion detection systems: a cross-domain overview. <i>Communications Surveys and Tutorials, IEEE Communications Society<\/i>, 2019, 21 (4), pp.3639 - 3681. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/COMST.2019.2922584\">&#x27E8;10.1109\/COMST.2019.2922584&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02403911v1\">&#x27E8;hal-02403911&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02403911v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2018<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Raphael Chane-Yack-Fa, Marc Frappier, Amel Mammar, Alain Finkel. Parameterized verification of monotone information systems. <i>Formal Aspects of Computing<\/i>, 2018, 30 (3-4), pp.463 - 489. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s00165-018-0460-8\">&#x27E8;10.1007\/s00165-018-0460-8&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01847131v1\">&#x27E8;hal-01847131&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-01847131\/file\/Chane-Yack-Fa2018.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01847131\/file\/Chane-Yack-Fa2018.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01847131\/file\/Chane-Yack-Fa2018.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01847131v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2017<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed Graiet, Lazhar Hamel, Amel Mammar, Samir Tata. A verification and deployment approach for elastic component-based applications. <i>Formal Aspects of Computing<\/i>, 2017, 29 (6), pp.987 - 1011. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s00165-017-0425-3\">&#x27E8;10.1007\/s00165-017-0425-3&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01692537v1\">&#x27E8;hal-01692537&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01692537v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed Graiet, Amel Mammar, Souha Boubaker, Walid Gaaloul. Towards correct cloud resource allocation in business processes. <i>IEEE Transactions on Services Computing<\/i>, 2017, 10 (1), pp.23 - 36. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/TSC.2016.2594062\">&#x27E8;10.1109\/TSC.2016.2594062&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01575735v1\">&#x27E8;hal-01575735&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01575735v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. Modeling a landing gear system in Event-B. <i>International Journal on Software Tools for Technology Transfer<\/i>, 2017, 19 (2), pp.167 - 186. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10009-015-0391-0\">&#x27E8;10.1007\/s10009-015-0391-0&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01254980v1\">&#x27E8;hal-01254980&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01254980v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Thi Mai Nguyen, R\u00e9gine Laleau. A formal approach to derive an aspect oriented programming-based implementation of a secure access control filter. <i>Information and Software Technology<\/i>, 2017, 92, pp.158 - 178. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.infsof.2017.08.001\">&#x27E8;10.1016\/j.infsof.2017.08.001&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01692569v1\">&#x27E8;hal-01692569&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01692569v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2016<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nghi Huynh, Marc Frappier, Amel Mammar, R\u00e9gine Laleau, Jules Desharnais. A formal validation of the RBAC ANSI 2012 standard using B. <i>Science of Computer Programming<\/i>, 2016, 131, pp.76 - 93. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.scico.2016.04.011\">&#x27E8;10.1016\/j.scico.2016.04.011&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01390991v1\">&#x27E8;hal-01390991&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01390991v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed-Anis Zemni, Amel Mammar, Nejib Ben Hadj Alouane. An automated approach for merging business process fragments. <i>Computers in Industry<\/i>, 2016, 82, pp.104 - 118. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.compind.2016.05.002\">&#x27E8;10.1016\/j.compind.2016.05.002&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01346029v1\">&#x27E8;hal-01346029&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01346029v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2015<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier. Proof-based verification approaches for dynamic properties : application to the information system domain. <i>Formal Aspects of Computing<\/i>, 2015, 27 (2), pp.335 - 374. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s00165-014-0323-x\">&#x27E8;10.1007\/s00165-014-0323-x&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01200474v1\">&#x27E8;hal-01200474&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01200474v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2012<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Natalia Kushik, Amel Mammar, Ana Rosa Cavalli, Nina Yevtushenko, Willy Ronald Jimenez Freitez, et al.. A SPIN-based approach for detecting vulnerabilities in C programs. <i>Automatic Control and Computer Sciences<\/i>, 2012, 46 (7), pp.379-386. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.3103\/S0146411612070115\">&#x27E8;10.3103\/S0146411612070115&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00772243v1\">&#x27E8;hal-00772243&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00772243v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Wissam Mallouli, Ana Rosa Cavalli. A systematic approach to integrate common timed security rules within a TEFSM-based system specification. <i>Information and Software Technology<\/i>, 2012, 54 (1), pp.87-98. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.infsof.2011.07.004\">&#x27E8;10.1016\/j.infsof.2011.07.004&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00711778v1\">&#x27E8;hal-00711778&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00711778v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nahid Shahmehri, Amel Mammar, Edgardo Montes de Oca, David Byers, Ana Rosa Cavalli, et al.. An advanced approach for modeling and detecting software vulnerabilities. <i>Information and Software Technology<\/i>, 2012, 54 (9), pp.997-1013. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.infsof.2012.03.004\">&#x27E8;10.1016\/j.infsof.2012.03.004&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00739075v1\">&#x27E8;hal-00739075&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00739075v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2009<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar. A systematic approach to generate B preconditions : application to the database domain. <i>Software and Systems Modeling<\/i>, 2009, 8 (3), pp.385-401. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10270-008-0098-8\">&#x27E8;10.1007\/s10270-008-0098-8&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00566987v1\">&#x27E8;hal-00566987&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00566987v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2008<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. Impl\u00e9mentation JAVA d'une sp\u00e9cification B: Application aux bases de donn\u00e9es. <i>Revue des Sciences et Technologies de l'Information - S\u00e9rie TSI : Technique et Science Informatiques<\/i>, 2008, 27 (5), pp.537--570. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01224657v1\">&#x27E8;hal-01224657&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01224657v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2006<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. From a B formal specification to an executable code: application to the relational database domain. <i>Information and Software Technology<\/i>, 2006, 28 (4), pp.253-279. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00145868v1\">&#x27E8;hal-00145868&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00145868v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. A formal approach based on UML and B for the specification and development of database applications. <i>Automated Software Engineering<\/i>, 2006, 13 (4), pp.497-528. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00147056v1\">&#x27E8;hal-00147056&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00147056v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. UB2SQL: A Tool for Building Database Applications Using UML and B Formal Method.. <i>Journal of Database Management<\/i>, 2006, 17 (4), pp.70-89. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01224665v1\">&#x27E8;hal-01224665&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01224665v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='Rubrique'>Communication dans un congr\u00e8s<\/p>\n<p class='SousRubrique'>2025<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Quelen Cartellier, Marc Frappier, Amel Mammar. A rodin plugin for generating proof obligations for invariant preservation for ASTDs. <i>The 23nd edition of the International Conference on Software Engineering and Formal Methods (SEFM)<\/i>, Nov 2025, Toledo, Spain. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-032-10444-1_10\">&#x27E8;10.1007\/978-3-032-10444-1_10&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-05445192v1\">&#x27E8;hal-05445192&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-05445192\/file\/SEFM2025.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-05445192\/file\/SEFM2025.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-05445192\/file\/SEFM2025.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-05445192v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2024<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Faycal Baba, Amel Mammar, Marc Frappier, R\u00e9gine Laleau. Modeling and Verification of Solidity Smart Contracts with the B Method. <i>Engineering of Complex Computer Systems<\/i>, Jun 2024, Limassol (Chypre), Cyprus. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04850532v1\">&#x27E8;hal-04850532&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04850532\/file\/Projet_ICECCS.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04850532\/file\/Projet_ICECCS.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04850532\/file\/Projet_ICECCS.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04850532v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar. An event-B model of a mechanical lung ventilator. <i>Rigorous State-Based Methods - 10th International Conference (ABZ)<\/i>, Jun 2024, Bergame (Italie), Italy. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-031-63790-2_25\">&#x27E8;10.1007\/978-3-031-63790-2_25&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04849848v1\">&#x27E8;hal-04849848&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04849848\/file\/ABZ2024CameraReady.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04849848\/file\/ABZ2024CameraReady.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04849848\/file\/ABZ2024CameraReady.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04849848v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Asfand Yar, Akram Idani, Yves Ledru, Simon Collart-Dutilleul, Amel Mammar, et al.. An iterative formal model-driven approach to railway systems validation. <i>28th International Conference on Engineering of Complex Computer Systems (ICECCS)<\/i>, Jun 2024, Limassol (Chypre), Cyprus. pp.272 - 289, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-031-66456-4_15\">&#x27E8;10.1007\/978-3-031-66456-4_15&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.univ-grenoble-alpes.fr\/hal-04731687v1\">&#x27E8;hal-04731687&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.univ-grenoble-alpes.fr\/hal-04731687\/file\/Chapter_Author.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.univ-grenoble-alpes.fr\/hal-04731687\/file\/Chapter_Author.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.univ-grenoble-alpes.fr\/hal-04731687\/file\/Chapter_Author.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.univ-grenoble-alpes.fr\/hal-04731687v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2023<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Meryem Afendi, Amel Mammar, R\u00e9gine Laleau. A tool-supported approach for modeling and verifying hybrid systems using EVENT-B and the differential equation solver SAGEMATH. <i>18th International Conference on Software Technologies (ICSOFT)<\/i>, Jul 2023, Rome, Italy. pp.71-83, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.5220\/0012080900003538\">&#x27E8;10.5220\/0012080900003538&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04344606v1\">&#x27E8;hal-04344606&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04344606\/file\/ICSOFT.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04344606\/file\/ICSOFT.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04344606\/file\/ICSOFT.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04344606v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Quelen Cartellier, Marc Frappier, Amel Mammar. Proving local invariants in ASTDs. <i>International Conference on Formal Engineering Methods (ICFEM )<\/i>, Nov 2023, Brisbane, QLD, Australia. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-981-99-7584-6_14\">&#x27E8;10.1007\/978-981-99-7584-6_14&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04344486v1\">&#x27E8;hal-04344486&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04344486\/file\/PO_ASTD_GRIC_Overleaf.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04344486\/file\/PO_ASTD_GRIC_Overleaf.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04344486\/file\/PO_ASTD_GRIC_Overleaf.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04344486v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Michael Leuschel. Modeling and verifying an arrival manager using event-B. <i>Rigorous State-Based Methods - 9th International Conference(ABZ)<\/i>, May 2023, Nancy, France. pp.21-339, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-031-33163-3_24\">&#x27E8;10.1007\/978-3-031-33163-3_24&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04192812v1\">&#x27E8;hal-04192812&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-04192812\/file\/ABZ2023.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04192812\/file\/ABZ2023.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04192812\/file\/ABZ2023.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04192812v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2022<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Meryem Afendi, Amel Mammar, R\u00e9gine Laleau. Building correct hybrid systems using Event-B and sagemath: Illustration by the hybrid smart heating system case study. <i>2022 26th International Conference on Engineering of Complex Computer Systems (ICECCS)<\/i>, Mar 2022, Hiroshima, Japan. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ICECCS54210.2022.00019\">&#x27E8;10.1109\/ICECCS54210.2022.00019&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/ip-paris.hal.science\/hal-03916803v1\">&#x27E8;hal-03916803&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/ip-paris.hal.science\/hal-03916803v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2020<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Meryem Afendi, R\u00e9gine Laleau, Amel Mammar. Modelling hybrid programs with event-B. <i>Rigorous State-Based Methods - 7th International Conference, ABZ<\/i>, May 2020, ULM, Germany. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-030-48077-6_10\">&#x27E8;10.1007\/978-3-030-48077-6_10&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-04851814v1\">&#x27E8;hal-04851814&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-04851814v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, R\u00e9gine Laleau. An Event-B model of an automotive adaptive exterior light system. <i>ABZ 2020: 7th international conference on Rigorous State-Based Methods<\/i>, May 2020, Ulm, Germany. pp.351-366, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-030-48077-6_28\">&#x27E8;10.1007\/978-3-030-48077-6_28&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02975783v1\">&#x27E8;hal-02975783&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02975783v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier. Modeling of a speed control system using Event-B. <i>ABZ 2020: 7th international conference on Rigorous State-Based Methods<\/i>, May 2020, Ulm, Germany. pp.367-381, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-030-48077-6_29\">&#x27E8;10.1007\/978-3-030-48077-6_29&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02975785v1\">&#x27E8;hal-02975785&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02975785v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Lionel Nganyewou Tidjon, Marc Frappier, Amel Mammar. Intrusion detection using ASTDs. <i>AINA 2020: 34th international conference on Advanced Information Networking and Applications<\/i>, Apr 2020, Caserta, Italy. pp.1397-1411, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-030-44041-1_118\">&#x27E8;10.1007\/978-3-030-44041-1_118&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02975779v1\">&#x27E8;hal-02975779&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02975779v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2019<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, R\u00e9gine Laleau, Marc Frappier, Amel Mammar, Francois Thibodeau, et al.. Assessment of a formal requirements modeling approach on a transportation system. <i>ICFEM 2019: 21st International Conference on Formal Engineering Methods<\/i>, Nov 2019, Shenzhen, China. pp.470-486, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-030-32409-4_29\">&#x27E8;10.1007\/978-3-030-32409-4_29&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02386946v1\">&#x27E8;hal-02386946&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02386946v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, R\u00e9gine Laleau, Hector Ruiz Barradas, Marc Frappier, Amel Mammar. A formal requirements modeling approach: application to rail communication. <i>ICSOFT 2019: 14th International Conference on Software Technologies<\/i>, Jul 2019, Prague, Czech Republic. pp.170-177, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.5220\/0007809701700177\">&#x27E8;10.5220\/0007809701700177&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02403931v1\">&#x27E8;hal-02403931&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-02403931v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2018<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, Amel Mammar, R\u00e9gine Laleau, Marc Frappier. Event-B expression and verification of translation rules between SysML\/KAOS domain models and B system specifications. <i>ABZ 2018 : 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z<\/i>, Jun 2018, Southampton, United Kingdom. pp.55--70, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-91271-4_5\">&#x27E8;10.1007\/978-3-319-91271-4_5&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01797812v1\">&#x27E8;hal-01797812&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01797812v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, Marc Frappier, R\u00e9gine Laleau, Amel Mammar. Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach. <i>Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings<\/i>, Jun 2018, Southampton, United Kingdom. pp.262-276, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-91271-4_18\">&#x27E8;10.1007\/978-3-319-91271-4_18&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01797811v1\">&#x27E8;hal-01797811&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01797811v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, R\u00e9gine Laleau. An Event-B model of the hybrid ERTMS\/ETCS level 3 standard. <i>Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings<\/i>, Jun 2018, Southampton, United Kingdom. pp.353-366, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-91271-4_24\">&#x27E8;10.1007\/978-3-319-91271-4_24&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01797810v1\">&#x27E8;hal-01797810&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01797810v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Lionel Tidjon, Marc Frappier, Michael Leuschel, Amel Mammar. Extended algebraic state-transition diagrams. <i>ICECCS 2018: 23rd International Conference on Engineering of Complex Computer Systems<\/i>, Dec 2018, Melbourne, Australia. pp.146 - 155, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ICECCS2018.2018.00023\">&#x27E8;10.1109\/ICECCS2018.2018.00023&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01963140v1\">&#x27E8;hal-01963140&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01963140v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Tueno, Marc Frappier, R\u00e9gine Laleau, Amel Mammar. Back propagating B system updates on SysML\/KAOS domain models. <i>ICECCS 2018: 23rd International Conference on Engineering of Complex Computer Systems<\/i>, Dec 2018, Melbourne, Australia. pp.160 - 169, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ICECCS2018.2018.00025\">&#x27E8;10.1109\/ICECCS2018.2018.00025&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01963152v1\">&#x27E8;hal-01963152&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01963152v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Tueno, Marc Frappier, R\u00e9gine Laleau, Amel Mammar, Michael Leuschel. Formalisation of SysML\/KAOS goal assignments with B system component decompositions. <i>IFM 2018: 14th International Conference on Integrated Formal Methods<\/i>, Sep 2018, Maynooth, Ireland. pp.377 - 397, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-98938-9_22\">&#x27E8;10.1007\/978-3-319-98938-9_22&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01885098v1\">&#x27E8;hal-01885098&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01885098v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2017<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nghi Huynh, Marc Frappier, Amel Mammar, R\u00e9gine Laleau. Verification of SGAC Access Control Policies Using Alloy and ProB. <i>18th IEEE International Symposium on High Assurance Systems Engineering, HASE 2017<\/i>, Jan 2017, Singapore, Singapore. pp.120 - 123, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/HASE.2017.24\">&#x27E8;10.1109\/HASE.2017.24&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01574899v1\">&#x27E8;hal-01574899&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01574899v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Tueno, R\u00e9gine Laleau, Amel Mammar, Marc Frappier. Towards using ontologies for domain modeling within the SysML\/KAOS approach. <i>REW 2017: IEEE 25th International Requirements Engineering Conference Workshops<\/i>, Sep 2017, Lisbon, Portugal. pp.1 - 5, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/REW.2017.22\">&#x27E8;10.1109\/REW.2017.22&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01692857v1\">&#x27E8;hal-01692857&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01692857v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2016<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Souha Boubaker, Amel Mammar, Mohamed Graiet, Walid Gaaloul. A formal guidance approach for correct process configuration. <i>ICSOC 2016 : 14th International Conference on Service-Oriented Computing<\/i>, Oct 2016, Banff, Canada. pp.483 - 498, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-46295-0_30\">&#x27E8;10.1007\/978-3-319-46295-0_30&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01425991v1\">&#x27E8;hal-01425991&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01425991v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Souha Boubaker, Amel Mammar, Mohamed Graiet, Walid Gaaloul. An event-B based approach for ensuring correct configurable business processes. <i>ICWS 2016 : 23rd IEEE International Conference on Web Services<\/i>, Jun 2016, San Francisco, United States. pp.460 - 467, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ICWS.2016.66\">&#x27E8;10.1109\/ICWS.2016.66&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01359893v1\">&#x27E8;hal-01359893&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01359893v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Souha Boubaker, Amel Mammar, Mohamed Graiet, Walid Gaaloul. Formal verification of cloud resource allocation in business processes using Event-B. <i>AINA 2016 : 30th International Conference on Advanced Information Networking and Applications<\/i>, Mar 2016, Crans-Montana, Switzerland. pp.746 - 753, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/AINA.2016.126\">&#x27E8;10.1109\/AINA.2016.126&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01341653v1\">&#x27E8;hal-01341653&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01341653v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nghi Huynh, Marc Frappier, Herman Pooda, Amel Mammar, R\u00e9gine Laleau. SGAC: a patient-centered access control method. <i>RCIS 2016 : 10th International Conference on Research Challenges in Information Science<\/i>, Jun 2016, Grenoble, France. pp.1 - 12, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/RCIS.2016.7549286\">&#x27E8;10.1109\/RCIS.2016.7549286&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01359877v1\">&#x27E8;hal-01359877&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01359877v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Thi Mai Nguyen, R\u00e9gine Laleau. Formal development of a secure access control filter. <i>HASE 2016 : 17th International Symposium on High-Assurance Systems Engineering<\/i>, Jan 2016, Orlando, Florida, United States. pp.173 - 180, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/HASE.2016.10\">&#x27E8;10.1109\/HASE.2016.10&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01298113v1\">&#x27E8;hal-01298113&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01298113v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. On the use of domain and system knowledge modeling in goal-based Event-B specifications. <i>ISOLA 2016 : 7th International Symposium on Leveraging Applications of Formal Methods<\/i>, Oct 2016, Corfu, Greece. pp.325 - 339, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-47166-2_23\">&#x27E8;10.1007\/978-3-319-47166-2_23&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01425977v1\">&#x27E8;hal-01425977&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01425977v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Thi Mai Nguyen, Amel Mammar, R\u00e9gine Laleau, Samir Hameg. A tool for the generation of a secure access control filter. <i>RCIS 2016 : 10th International Conference on Research Challenges in Information Science<\/i>, Jun 2016, Grenoble, France. pp.1 - 12, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/RCIS.2016.7549285\">&#x27E8;10.1109\/RCIS.2016.7549285&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01359879v1\">&#x27E8;hal-01359879&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01359879v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2014<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Fama Diagne, Amel Mammar, Marc Frappier. A tool for verifying dynamic properties in B. <i>SEFM 2014 : 12th International Conference on Software Engineering and Formal Methods<\/i>, Sep 2014, Grenoble, France. pp.290 - 295, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-10431-7_23\">&#x27E8;10.1007\/978-3-319-10431-7_23&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01264805v1\">&#x27E8;hal-01264805&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01264805v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Nghi Huynh, Marc Frappier, Amel Mammar, R\u00e9gine Laleau, Jules Desharnais. Validating the RBAC ANSI 2012 standard using B. <i>ABZ 2014 : 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z<\/i>, Jun 2014, Toulouse, France. pp.255 - 270, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-662-43652-3_22\">&#x27E8;10.1007\/978-3-662-43652-3_22&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01264810v1\">&#x27E8;hal-01264810&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01264810v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier. Verifying the precedence property pattern using the B Method. <i>HASE 2014 : 15th International Symposium on High Assurance System Engineering<\/i>, Jan 2014, Miami, United States. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/HASE.2014.40\">&#x27E8;10.1109\/HASE.2014.40&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00958505v1\">&#x27E8;hal-00958505&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00958505v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. Modeling a landing gear system in Event-B. <i>ABZ 2014 : 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z<\/i>, Jun 2014, Toulouse, France. pp.80 - 94, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-07512-9_6\">&#x27E8;10.1007\/978-3-319-07512-9_6&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01254981v1\">&#x27E8;hal-01254981&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01254981v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. A proved approach for building correct instances of UML associations : multiplicities satisfaction. <i>APSEC 2014 : 21st Asia-Pacific Software Engineering Conference<\/i>, Dec 2014, Jeju, South Korea. pp.438 - 445, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/APSEC.2014.103\">&#x27E8;10.1109\/APSEC.2014.103&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01257892v1\">&#x27E8;hal-01257892&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01257892v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed-Anis Zemni, Nejib Ben Hadj Alouane, Amel Mammar. Business process fragments behavioral merge. <i>COOPIS 2014 : International Conference on Cooperative Information Systems<\/i>, Oct 2014, Amantea, Italy. pp.112 - 129, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-662-45563-0_7\">&#x27E8;10.1007\/978-3-662-45563-0_7&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01263178v1\">&#x27E8;hal-01263178&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01263178v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed-Anis Zemni, Amel Mammar, Nejib Ben Hadj Alouane. A behavior-aware systematic approach for merging business process fragments. <i>ICECCS 2014 : 19th International Conference on Engineering of Complex Computer Systems<\/i>, Aug 2014, Tianjin, China. pp.194 - 197, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ICECCS.2014.35\">&#x27E8;10.1109\/ICECCS.2014.35&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01264795v1\">&#x27E8;hal-01264795&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01264795v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed-Anis Zemni, Amel Mammar, Nejib Ben Hadj Alouane. Formal approach for generating privacy preserving user requirements-based business process fragments. <i>ACSC 2014 : 37th Australasian Computer Science Conference <\/i>, Jan 2014, Auckland, New Zealand. pp.89 - 98. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01290711v1\">&#x27E8;hal-01290711&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01290711v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2013<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mohamed-Anis Zemni, Nejib Ben Hadj Alouane, Amel Mammar. Process decomposition based on semantics and privacy-aware requirements-driven approach. <i>IIWAS 2013 : 15 th International Conference on Information Integration and Web-based Applications & Services<\/i>, Dec 2013, Vienna, Austria. pp.654 - 657, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1145\/2539150.2539258\">&#x27E8;10.1145\/2539150.2539258&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01263179v1\">&#x27E8;hal-01263179&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01263179v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2012<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Marc Frappier, Amel Mammar. An assertions-based approach to verifying the absence property pattern. <i>23rd IEEE International Symposium on Software Reliability Engineering (ISSRE'12)<\/i>, Nov 2012, Dallas, TX, United States. pp.361-370, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/ISSRE.2012.11\">&#x27E8;10.1109\/ISSRE.2012.11&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00816403v1\">&#x27E8;hal-00816403&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00816403v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, Raphael Chane-Yack-Fa. Proving the absence property pattern using the B method. <i>HASE 2012 : 14th IEEE International High Assurance Systems Engineering Symposium<\/i>, Oct 2012, Omaha, United States. pp.167-170, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/HASE.2012.26\">&#x27E8;10.1109\/HASE.2012.26&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00767744v1\">&#x27E8;hal-00767744&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-00767744\/file\/mammar2012.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-00767744\/file\/mammar2012.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-00767744\/file\/mammar2012.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-00767744v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2011<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Marc Frappier, Amel Mammar. Proving non-interference on reachability properties : a refinement approach. <i>APSEC 2011 : 18th Asia Pacific Software Engineering Conference<\/i>, Dec 2011, Ho Chi Minh, Vietnam. pp.25 - 32, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/APSEC.2011.35\">&#x27E8;10.1109\/APSEC.2011.35&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01302414v1\">&#x27E8;hal-01302414&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01302414v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Mariem Graa, Nora Cuppens-Boulahia, Fabien Autrel, Hanieh Azkia, Fr\u00e9d\u00e9ric Cuppens, et al.. Using requirements engineering in an automatic security policy derivation process. <i>DPM - SETOP 2011 : 6th International Workshop on Data Privacy Management and 4th International Workshop on Autonomous and Spontaneous Security<\/i>, Sep 2011, Leuven, Belgium. pp.155-172, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-642-28879-1_11\">&#x27E8;10.1007\/978-3-642-28879-1_11&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00738844v1\">&#x27E8;hal-00738844&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00738844v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Natalia Kushik, Amel Mammar, Ana Rosa Cavalli, Nina Yevtushenko, Edgardo Montes de Oca. A SPIN-based approach for detecting vulnerabilities in C programs. <i>PSSV 2011 : 2nd Workshop on Program Semantics, Specification and Verification : Theory and Applications<\/i>, Jun 2011, St Petersburg, Russia. pp.131 - 143. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01465027v1\">&#x27E8;hal-01465027&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01465027v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar. An overview of a proof-based approach to detecting C vulnerabilities. <i>SAC 2011 : 26th Symposium on Applied Computing<\/i>, Mar 2011, Taichung, Taiwan. pp.1343 - 1344, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1145\/1982185.1982476\">&#x27E8;10.1145\/1982185.1982476&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01303015v1\">&#x27E8;hal-01303015&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01303015v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Marc Frappier, Fama Diagne. A proof-based approach to verifying reachability properties. <i>SAC 2011 : 26th Symposium on Applied Computing<\/i>, Mar 2011, Taichung, Taiwan. pp.1651 - 1657, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1145\/1982185.1982531\">&#x27E8;10.1145\/1982185.1982531&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01303017v1\">&#x27E8;hal-01303017&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01303017v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Ana Rosa Cavalli, Willy Ronald Jimenez Freitez, Wissam Mallouli, Edgardo Montes de Oca. Using testing techniques for vulnerability detection in C programs. <i>23th International Conference on Testing Software and Systems (ICTSS)<\/i>, Nov 2011, Paris, France. pp.80-96, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-642-24580-0_7\">&#x27E8;10.1007\/978-3-642-24580-0_7&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01303013v1\">&#x27E8;hal-01303013&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-01303013\/file\/978-3-642-24580-0_7_Chapter.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01303013\/file\/978-3-642-24580-0_7_Chapter.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01303013\/file\/978-3-642-24580-0_7_Chapter.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01303013v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Pengfei Liu. A proof-based approach to detect vulnerabilities in C programs. <i>SERP 2011 : International Conference on Software Engineering Research and Practice<\/i>, Jul 2011, Las Vegas, United States. pp.464 - 470. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01302477v1\">&#x27E8;hal-01302477&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-01302477\/file\/Mammar2011.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01302477\/file\/Mammar2011.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01302477\/file\/Mammar2011.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01302477v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2010<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Marc Frappier, Fama Diagne, Amel Mammar. Proving reachability in B using substitution refinement. <i>WOBD 2010 : Workshop on B Dissemination<\/i>, Nov 2010, Natal, Brazil. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01306195v1\">&#x27E8;hal-01306195&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01306195v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Fama Diagne, Marc Frappier. A proof-based approach to verifying reachability properties. <i>WOBD 2010 : Workshop on B Dissemination<\/i>, Nov 2010, Natal, Brazil. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01306183v1\">&#x27E8;hal-01306183&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01306183v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2009<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Willy Ronald Jimenez Freitez, Amel Mammar, Ana Rosa Cavalli. Software vulnerabilities, prevention and detection methods : a review. <i>SEC-MDA 2009 : Security in Model Driven Architecture <\/i>, Jun 2009, Enschede, Netherlands. pp.1 - 11. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01367445v1\">&#x27E8;hal-01367445&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-01367445\/file\/GET_sec-mda09.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01367445\/file\/GET_sec-mda09.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01367445\/file\/GET_sec-mda09.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01367445v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Wissam Mallouli, Amel Mammar, Ana Rosa Cavalli. A formal framework to integrate timed security rules within a TEFSM-based system specification. <i>APSEC 2009 : 16th AsiaPacific Software Engineering Conference<\/i>, Dec 2009, Batu Ferringhi, Malaysia. pp.489 - 496, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/APSEC.2009.52\">&#x27E8;10.1109\/APSEC.2009.52&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00444089v1\">&#x27E8;hal-00444089&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-00444089\/file\/mallouli2009.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-00444089\/file\/mallouli2009.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-00444089\/file\/mallouli2009.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-00444089v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Wissam Mallouli, Amel Mammar, Ana Cavalli. Prise en Compte de R\u00e8gles de S\u00e9curit\u00e9 Temporelles dans une Sp\u00e9ci\ufb01cation TEFSM d'un Syst\u00e8me. <i>CFIP'2009<\/i>, Oct 2009, Strasbourg, France. <a target=\"_blank\" href=\"https:\/\/inria.hal.science\/inria-00419463v1\">&#x27E8;inria-00419463&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/inria.hal.science\/inria-00419463\/file\/34.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/inria-00419463\/file\/34.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/inria-00419463\/file\/34.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/inria-00419463v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Ana Rosa Cavalli, Edgardo Montes de Oca, Shanai Ardi, David Byers, et al.. Mod\u00e9lisation et d\u00e9tection formelles de vuln\u00e9rabilit\u00e9s logicielles par le test passif. <i>SAR-SSI 2009 : 4eme Conf\u00e9rence sur la S\u00e9curit\u00e9 des Architectures R\u00e9seaux et des Syst\u00e8mes d'Information <\/i>, Jun 2009, Luchon, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00444066v1\">&#x27E8;hal-00444066&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00444066v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2008<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Salimeh Behnia, Amel Mammar, Jean-Marc Mota, Nicolas Breton, Paul Caspi, et al.. Industrialising a proof-based verification approach of computerised interlocking systems. <i>COMPRAIL '08 : Eleventh International Conference on Computer System Design and Operation in the Railway and Other Transit Systems<\/i>, Sep 2008, Toledo, Spain. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.2495\/CR080151\">&#x27E8;10.2495\/CR080151&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00796378v1\">&#x27E8;hal-00796378&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00796378v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Wissam Mallouli, Amel Mammar, Ana Rosa Cavalli. Modeling system security rules with time constraints using timed extended finite state machines. <i>DS-RT 2008 : 12th IEEE\/ACM International Symposium on Distributed Simulation an Real Time Applications<\/i>, Oct 2008, Vancouver, Canada. pp.173 - 180, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/DS-RT.2008.22\">&#x27E8;10.1109\/DS-RT.2008.22&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01380237v1\">&#x27E8;hal-01380237&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01380237v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2006<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, Fr\u00e9d\u00e9ric Gervais, R\u00e9gine Laleau. Systematic Identification of Preconditions from Set-Based Integrity Constraints. <i>INFORSID'06, Hammamet, Tunisie<\/i>, Jan 2006, X, France. pp.595-610. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01125172v1\">&#x27E8;hal-01125172&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01125172v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2004<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. UML2SQL: Un environment int\u00e9gr\u00e9 pour le d\u00e9veloppement d'impl\u00e9mentations relationnelles \u00e0 partir de diagrammes UML. <i>AFADL'04<\/i>, Jan 2004, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124911v1\">&#x27E8;hal-01124911&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124911v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. UML2SQL : un environnement int\u00e9gr\u00e9 pour le d\u00e9veloppement d'impl\u00e9mentations relationnelles \u00e0 partir de diagrammes UML. <i>Approches Formelles dans l'Assistance au D\u00e9veloppement de Logiciels, AFADL'04<\/i>, 2004, Besan\u00c3\u00a7on, France. pp.333--336. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01224669v1\">&#x27E8;hal-01224669&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01224669v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. G\u00e9n\u00e9ration de code ex\u00e9cutable \u00e0 partir d'une sp\u00e9cification B : applications aux bases de donn\u00e9es. <i>Approches Formelles dans l'Assistance au D\u00e9veloppement de Logiciels, AFADL'04<\/i>, 2004, Besan\u00c3\u00a7on, France. pp.77--91. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01224671v1\">&#x27E8;hal-01224671&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01224671v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. G\u00e9n\u00e9ration de code \u00e0 partir d'une sp\u00e9cification B:  application aux bases de donn\u00e9es. <i>AFADL'04<\/i>, Jan 2004, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124909v1\">&#x27E8;hal-01124909&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124909v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2003<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. Design of an Automatic Prover Dedicated to the Refinement of Database Applications. <i>FM'2003, Springer-Verlag, LNCS n\u00b0 2805, pp 834-854, Pise,Italy<\/i>, Jan 2003, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124709v1\">&#x27E8;hal-01124709&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124709v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2001<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. An Automatic Generation of B Specifications from Well-defined UML Notations for Database Applications. <i>Int. Symp. on Programming Systems, Alger, Alg\u00e9rie<\/i>, Jan 2001, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124660v1\">&#x27E8;hal-01124660&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124660v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar. Une approche formelle par raffinement pour le d\u00e9veloppement d'applications bases de donn\u00e9es s\u00fbres. <i>19\u00e8me congr\u00e9s INFORSID, Gen\u00e8ve, Suisse<\/i>, Jan 2001, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124663v1\">&#x27E8;hal-01124663&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124663v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2000<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. An Overview of a Method and its support Tool for Generating B Specifications from UML Notations. <i>15th IEEE Int. Conf. on Automated Software Engineering (ASE2000), Grenoble, France<\/i>, Jan 2000, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124519v1\">&#x27E8;hal-01124519&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124519v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. A Generic Process to Refine a B Specification into a Relational Database Implementation. <i>First Int. Conf. of B and Z users (ZB2000), Springer-Verlag, LNCS n\u00b0 1878, York, UK<\/i>, Jan 2000, X, France. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124529v1\">&#x27E8;hal-01124529&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124529v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='Rubrique'>Chapitre d'ouvrage<\/p>\n<p class='SousRubrique'>2021<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, R\u00e9gine Laleau, Amel Mammar, Marc Frappier. Integrating domain modeling within a formal requirements engineering method. <i>Implicit and explicit semantics integration in proof-based developments of discrete systems: communications of NII Shonan meetings<\/i>, Springer, pp.39-58, 2021, 978-981-15-5053-9. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-981-15-5054-6_3\">&#x27E8;10.1007\/978-981-15-5054-6_3&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-03545897v1\">&#x27E8;hal-03545897&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-03545897v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2014<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Jean-Marc Mota, Evguenia Dmitrieva, Amel Mammar, Paul Caspi, Nicolas Breton, et al.. Safety demonstration for a rail signaling application in nominal and degraded modes using formal proof. <i>Formal methods applied to complex systems<\/i>, ISTE-Wiley, pp.71 - 113, 2014, Computer Engineering Series, 978-1-84821-632-7. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1002\/9781119004707.ch4\">&#x27E8;10.1002\/9781119004707.ch4&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01464432v1\">&#x27E8;hal-01464432&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01464432v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2012<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Jean-Marc Mota, Evguenia Dmitrieva, Amel Mammar, Paul Caspi, Salimeh Behnia, et al.. D\u00e9monstration de la s\u00e9curit\u00e9 d'une application de signalisation en mode nominal et en modes d\u00e9grad\u00e9s par la preuve formelle. <i>Techniques industrielles de mod\u00e9lisation formelle pour le transport<\/i>, Hermes-Lavoisier, pp.145-185, 2012, 978-2-7462-3230-3. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00766909v1\">&#x27E8;hal-00766909&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00766909v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Jean-Marc Mota, Evguenia Dmitrieva, Amel Mammar, Paul Caspi, Salimeh Behnia, et al.. D\u00e9monstration de la s\u00e9curit\u00e9 d'une application de signalisation en mode nominal et en modes d\u00e9grad\u00e9s par la preuve formelle. <i>Techniques industrielles de mod\u00e9lisation formelle pour le transport<\/i>, Herm\u00e8s-Lavoisier, pp.145-185, 2012, 978-2-7462-3230-3. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00796381v1\">&#x27E8;hal-00796381&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00796381v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2010<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Wissam Mallouli, Mounir Lallali, Amel Mammar, Gerardo Morales, Ana Rosa Cavalli. Modeling and testing secure web applications. <i>Web-based information technologies and distributed systems<\/i>, Atlantis Press, pp.207-255, 2010, Atlantis Ambient and Pervasive Intelligence, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-94-91216-32-9_10\">&#x27E8;10.1007\/978-94-91216-32-9_10&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00673835v1\">&#x27E8;hal-00673835&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00673835v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2009<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. UB2SQL : a tool for building database applications using UML and B formal method. <i>Database technologies : concepts, methodologies, tools, and applications<\/i>, IGI Global, pp.1168-1188, 2009, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.4018\/978-1-60566-058-5.ch067\">&#x27E8;10.4018\/978-1-60566-058-5.ch067&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00597321v1\">&#x27E8;hal-00597321&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00597321v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2008<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Amel Mammar, R\u00e9gine Laleau. UB2SQL : a tool for building database applications using UML and B formal method. <i>Advanced principles for improving database design, systems modeling, and software development<\/i>, Information Science Publishing, pp.111 - 131, 2008, Advances in Database Research, 978-1-60566-172-8. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.4018\/978-1-60566-172-8.ch007\">&#x27E8;10.4018\/978-1-60566-172-8.ch007&#x27E9;<\/a>. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01326381v1\">&#x27E8;hal-01326381&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01326381v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2006<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. From UML Diagrams to B Specifications. Henri Habrias, France Marc Frappier. <i>Software Specification Methods : an Overview Using a Case Study<\/i>, ISTE - London, pp.59 - 80, 2006. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-00145958v1\">&#x27E8;hal-00145958&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-00145958v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='Rubrique'>Rapport<\/p>\n<p class='SousRubrique'>2019<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Steve Jeffrey Tueno Fotso, Amel Mammar, R\u00e9gine Laleau, Marc Frappier. Formal representation of SysML\/KAOS domain model. [Research Report] LACL, Universit\u00e9 Paris-Est\/Cr\u00e9teil. 2019. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-02874826v1\">&#x27E8;hal-02874826&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\">\n<a href=\"https:\/\/hal.science\/hal-02874826\/file\/Domain_Model_Formalization-formal_syntax_for_rules-Mars2019.pdf\"  target=\"_blank\">\n<img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-02874826\/file\/Domain_Model_Formalization-formal_syntax_for_rules-Mars2019.pdf\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-02874826\/file\/Domain_Model_Formalization-formal_syntax_for_rules-Mars2019.pdf\" \/><\/a>\n<span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-02874826v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>2004<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. UML2SQL: An Integrated Environment for the Development of UML and SQL Specifications. [Research Report] CEDRIC-04-643, CEDRIC Lab\/CNAM. 2004. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124913v1\">&#x27E8;hal-01124913&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124913v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2001<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. R\u00e9utilisation des preuves dans le processus de raffinement B. [Research Report] CEDRIC-01-377, CEDRIC Lab\/CNAM. 2001. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124730v1\">&#x27E8;hal-01124730&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124730v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. Un exemple de g\u00e9n\u00e9ration d'une impl\u00e9mentation relationnelle \u00e0 partir d'une sp\u00e9cification B. [Research Report] CEDRIC-01-368, CEDRIC Lab\/CNAM. 2001. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124723v1\">&#x27E8;hal-01124723&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124723v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>2000<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">R\u00e9gine Laleau, Amel Mammar. Using a Formal Refinement to Derive Relational Database Implementations from B Specifications. [Research Report] CEDRIC-00-86, CEDRIC Lab\/CNAM. 2000. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124516v1\">&#x27E8;hal-01124516&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124516v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<p class='SousRubrique'>1999<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Philippe Facon, R\u00e9gine Laleau, Amel Mammar, Fiona Polack. Formal Specification of the UML Metamodel for Building Rigorous Caise Tools. [Research Report] CEDRIC-99-91, CEDRIC Lab\/CNAM. 1999. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124520v1\">&#x27E8;hal-01124520&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124520v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">ref_biblio<\/dt><dd class=\"ValeurRes ref_biblio\">Philippe Facon, R\u00e9gine Laleau, Amel Mammar. Combining UML with the B Formal Method for the Specification of Database Applications. [Research Report] CEDRIC-99-87, CEDRIC Lab\/CNAM. 1999. <a target=\"_blank\" href=\"https:\/\/hal.science\/hal-01124517v1\">&#x27E8;hal-01124517&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\">\n<a href=\"https:\/\/hal.science\/hal-01124517v1\/bibtex\" target=\"_self\">\n<img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.archives-ouvertes.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a>\n<\/dd>\n<\/dl>\n<\/div>\n<\/p>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":4,"featured_media":4293,"parent":2438,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"ocean_post_layout":"","ocean_both_sidebars_style":"","ocean_both_sidebars_content_width":0,"ocean_both_sidebars_sidebars_width":0,"ocean_sidebar":"0","ocean_second_sidebar":"0","ocean_disable_margins":"enable","ocean_add_body_class":"","ocean_shortcode_before_top_bar":"","ocean_shortcode_after_top_bar":"","ocean_shortcode_before_header":"","ocean_shortcode_after_header":"","ocean_has_shortcode":"","ocean_shortcode_after_title":"","ocean_shortcode_before_footer_widgets":"","ocean_shortcode_after_footer_widgets":"","ocean_shortcode_before_footer_bottom":"","ocean_shortcode_after_footer_bottom":"","ocean_display_top_bar":"default","ocean_display_header":"default","ocean_header_style":"","ocean_center_header_left_menu":"0","ocean_custom_header_template":"0","ocean_custom_logo":0,"ocean_custom_retina_logo":0,"ocean_custom_logo_max_width":0,"ocean_custom_logo_tablet_max_width":0,"ocean_custom_logo_mobile_max_width":0,"ocean_custom_logo_max_height":0,"ocean_custom_logo_tablet_max_height":0,"ocean_custom_logo_mobile_max_height":0,"ocean_header_custom_menu":"0","ocean_menu_typo_font_family":"0","ocean_menu_typo_font_subset":"","ocean_menu_typo_font_size":0,"ocean_menu_typo_font_size_tablet":0,"ocean_menu_typo_font_size_mobile":0,"ocean_menu_typo_font_size_unit":"px","ocean_menu_typo_font_weight":"","ocean_menu_typo_font_weight_tablet":"","ocean_menu_typo_font_weight_mobile":"","ocean_menu_typo_transform":"","ocean_menu_typo_transform_tablet":"","ocean_menu_typo_transform_mobile":"","ocean_menu_typo_line_height":0,"ocean_menu_typo_line_height_tablet":0,"ocean_menu_typo_line_height_mobile":0,"ocean_menu_typo_line_height_unit":"","ocean_menu_typo_spacing":0,"ocean_menu_typo_spacing_tablet":0,"ocean_menu_typo_spacing_mobile":0,"ocean_menu_typo_spacing_unit":"","ocean_menu_link_color":"","ocean_menu_link_color_hover":"","ocean_menu_link_color_active":"","ocean_menu_link_background":"","ocean_menu_link_hover_background":"","ocean_menu_link_active_background":"","ocean_menu_social_links_bg":"","ocean_menu_social_hover_links_bg":"","ocean_menu_social_links_color":"","ocean_menu_social_hover_links_color":"","ocean_disable_title":"default","ocean_disable_heading":"default","ocean_post_title":"","ocean_post_subheading":"","ocean_post_title_style":"","ocean_post_title_background_color":"","ocean_post_title_background":0,"ocean_post_title_bg_image_position":"","ocean_post_title_bg_image_attachment":"","ocean_post_title_bg_image_repeat":"","ocean_post_title_bg_image_size":"","ocean_post_title_height":0,"ocean_post_title_bg_overlay":0.5,"ocean_post_title_bg_overlay_color":"","ocean_disable_breadcrumbs":"default","ocean_breadcrumbs_color":"","ocean_breadcrumbs_separator_color":"","ocean_breadcrumbs_links_color":"","ocean_breadcrumbs_links_hover_color":"","ocean_display_footer_widgets":"default","ocean_display_footer_bottom":"default","ocean_custom_footer_template":"0","footnotes":""},"class_list":["post-3524","page","type-page","status-publish","has-post-thumbnail","hentry","entry","has-media"],"_links":{"self":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/pages\/3524","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/comments?post=3524"}],"version-history":[{"count":1,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/pages\/3524\/revisions"}],"predecessor-version":[{"id":3525,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/pages\/3524\/revisions\/3525"}],"up":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/pages\/2438"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media\/4293"}],"wp:attachment":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media?parent=3524"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}