A formal validation of the RBAC ANSI 2012 standard using B

We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is pr...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2016-12, Vol.131, p.76-93
Main Authors: Huynh, Nghi, Frappier, Marc, Mammar, Amel, Laleau, Régine, Desharnais, Jules
Format: Article
Language:English
Subjects:
B method
Computer Science
Invariant preservation
Role-Based Access Control
Software Engineering
Symbolic Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83
cites cdi_FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83
container_end_page 93
container_issue
container_start_page 76
container_title Science of computer programming
container_volume 131
creator Huynh, Nghi
Frappier, Marc
Mammar, Amel
Laleau, Régine
Desharnais, Jules
description We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.
doi_str_mv 10.1016/j.scico.2016.04.011
format article
fullrecord <record><control><sourceid>elsevier_hal_p</sourceid><recordid>TN_cdi_hal_primary_oai_HAL_hal_01390991v1</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><els_id>S016764231630020X</els_id><sourcerecordid>S016764231630020X</sourcerecordid><originalsourceid>FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83</originalsourceid><addsrcrecordid>eNp9kEtLxDAUhYMoOI7-AjfZumjNTdq0EVx0BnUGBgUf65Dm4WTotJLUgv_e1hGXri733vMdOAehSyApEODXuzRqr7uUjktKspQAHKEZlAVNCsGzYzQbH0XCM8pO0VmMO0IIzwqYoZsKuy7sVYMH1Xijet-1uHO431r8vKiWuHp8WePRl-LYq9aoYPBn9O07XpyjE6eaaC9-5xy93d-9LlfJ5ulhvaw2iWYl7ZM8q2taF4bmXDkKlJlc14zVvBbW6tJppZ0ogedO09KRPNO5EOBAq1LYWpVsjq4OvlvVyI_g9yp8yU55uao2croRYIKMzACjlh20OnQxBuv-ACByqkru5E9VcqpKkmyEJ-r2QNkxxuBtmDS21db4YHUvTef_5b8B2MVwKQ</addsrcrecordid><sourcetype>Open Access Repository</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>A formal validation of the RBAC ANSI 2012 standard using B</title><source>ScienceDirect Journals</source><creator>Huynh, Nghi ; Frappier, Marc ; Mammar, Amel ; Laleau, Régine ; Desharnais, Jules</creator><creatorcontrib>Huynh, Nghi ; Frappier, Marc ; Mammar, Amel ; Laleau, Régine ; Desharnais, Jules</creatorcontrib><description>We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.</description><identifier>ISSN: 0167-6423</identifier><identifier>EISSN: 1872-7964</identifier><identifier>DOI: 10.1016/j.scico.2016.04.011</identifier><language>eng</language><publisher>Elsevier B.V</publisher><subject>B method ; Computer Science ; Invariant preservation ; Role-Based Access Control ; Software Engineering ; Symbolic Computation</subject><ispartof>Science of computer programming, 2016-12, Vol.131, p.76-93</ispartof><rights>2016 Elsevier B.V.</rights><rights>Distributed under a Creative Commons Attribution 4.0 International License</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83</citedby><cites>FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83</cites><orcidid>0000-0003-0016-6898 ; 0000-0002-2019-4936</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>230,314,776,780,881,27903,27904</link.rule.ids><backlink>$$Uhttps://hal.science/hal-01390991$$DView record in HAL$$Hfree_for_read</backlink></links><search><creatorcontrib>Huynh, Nghi</creatorcontrib><creatorcontrib>Frappier, Marc</creatorcontrib><creatorcontrib>Mammar, Amel</creatorcontrib><creatorcontrib>Laleau, Régine</creatorcontrib><creatorcontrib>Desharnais, Jules</creatorcontrib><title>A formal validation of the RBAC ANSI 2012 standard using B</title><title>Science of computer programming</title><description>We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.</description><subject>B method</subject><subject>Computer Science</subject><subject>Invariant preservation</subject><subject>Role-Based Access Control</subject><subject>Software Engineering</subject><subject>Symbolic Computation</subject><issn>0167-6423</issn><issn>1872-7964</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2016</creationdate><recordtype>article</recordtype><recordid>eNp9kEtLxDAUhYMoOI7-AjfZumjNTdq0EVx0BnUGBgUf65Dm4WTotJLUgv_e1hGXri733vMdOAehSyApEODXuzRqr7uUjktKspQAHKEZlAVNCsGzYzQbH0XCM8pO0VmMO0IIzwqYoZsKuy7sVYMH1Xijet-1uHO431r8vKiWuHp8WePRl-LYq9aoYPBn9O07XpyjE6eaaC9-5xy93d-9LlfJ5ulhvaw2iWYl7ZM8q2taF4bmXDkKlJlc14zVvBbW6tJppZ0ogedO09KRPNO5EOBAq1LYWpVsjq4OvlvVyI_g9yp8yU55uao2croRYIKMzACjlh20OnQxBuv-ACByqkru5E9VcqpKkmyEJ-r2QNkxxuBtmDS21db4YHUvTef_5b8B2MVwKQ</recordid><startdate>20161201</startdate><enddate>20161201</enddate><creator>Huynh, Nghi</creator><creator>Frappier, Marc</creator><creator>Mammar, Amel</creator><creator>Laleau, Régine</creator><creator>Desharnais, Jules</creator><general>Elsevier B.V</general><general>Elsevier</general><scope>AAYXX</scope><scope>CITATION</scope><scope>1XC</scope><orcidid>https://orcid.org/0000-0003-0016-6898</orcidid><orcidid>https://orcid.org/0000-0002-2019-4936</orcidid></search><sort><creationdate>20161201</creationdate><title>A formal validation of the RBAC ANSI 2012 standard using B</title><author>Huynh, Nghi ; Frappier, Marc ; Mammar, Amel ; Laleau, Régine ; Desharnais, Jules</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2016</creationdate><topic>B method</topic><topic>Computer Science</topic><topic>Invariant preservation</topic><topic>Role-Based Access Control</topic><topic>Software Engineering</topic><topic>Symbolic Computation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Huynh, Nghi</creatorcontrib><creatorcontrib>Frappier, Marc</creatorcontrib><creatorcontrib>Mammar, Amel</creatorcontrib><creatorcontrib>Laleau, Régine</creatorcontrib><creatorcontrib>Desharnais, Jules</creatorcontrib><collection>CrossRef</collection><collection>Hyper Article en Ligne (HAL)</collection><jtitle>Science of computer programming</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Huynh, Nghi</au><au>Frappier, Marc</au><au>Mammar, Amel</au><au>Laleau, Régine</au><au>Desharnais, Jules</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>A formal validation of the RBAC ANSI 2012 standard using B</atitle><jtitle>Science of computer programming</jtitle><date>2016-12-01</date><risdate>2016</risdate><volume>131</volume><spage>76</spage><epage>93</epage><pages>76-93</pages><issn>0167-6423</issn><eissn>1872-7964</eissn><abstract>We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.</abstract><pub>Elsevier B.V</pub><doi>10.1016/j.scico.2016.04.011</doi><tpages>18</tpages><orcidid>https://orcid.org/0000-0003-0016-6898</orcidid><orcidid>https://orcid.org/0000-0002-2019-4936</orcidid><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0167-6423
ispartof Science of computer programming, 2016-12, Vol.131, p.76-93
issn 0167-6423
1872-7964
language eng
recordid cdi_hal_primary_oai_HAL_hal_01390991v1
source ScienceDirect Journals
subjects B method
Computer Science
Invariant preservation
Role-Based Access Control
Software Engineering
Symbolic Computation
title A formal validation of the RBAC ANSI 2012 standard using B
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-27T17%3A56%3A25IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-elsevier_hal_p&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=A%20formal%20validation%20of%20the%20RBAC%20ANSI%202012%20standard%20using%20B&rft.jtitle=Science%20of%20computer%20programming&rft.au=Huynh,%20Nghi&rft.date=2016-12-01&rft.volume=131&rft.spage=76&rft.epage=93&rft.pages=76-93&rft.issn=0167-6423&rft.eissn=1872-7964&rft_id=info:doi/10.1016/j.scico.2016.04.011&rft_dat=%3Celsevier_hal_p%3ES016764231630020X%3C/elsevier_hal_p%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c382t-54bb2b7d256af2123d5cb33b6b9eec8fcacf98165fc28f054c5991f1ca89eba83%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true