A formal validation of the RBAC ANSI 2012 standard using B.

Saved in:
Bibliographic Details
Title: A formal validation of the RBAC ANSI 2012 standard using B.
Authors: Huynh, Nghi1,2 nghi.huynh@usherbrooke.ca, Frappier, Marc1 marc.frappier@usherbrooke.ca, Mammar, Amel3 amel.mammar@telecom-sudparis.eu, Laleau, Régine2 laleau@u-pec.fr, Desharnais, Jules4 Jules.Desharnais@ift.ulaval.ca
Source: Science of Computer Programming. Dec2016, Vol. 131, p76-93. 18p.
Subjects: B method (Computer science), ANSI standards, Inconsistency (Logic), Mathematical notation, Ad hoc computer networks, Access control
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 FROM AUTHOR]
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 118898535
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A formal validation of the RBAC ANSI 2012 standard using B.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Huynh%2C+Nghi%22">Huynh, Nghi</searchLink><relatesTo>1,2</relatesTo><i> nghi.huynh@usherbrooke.ca</i><br /><searchLink fieldCode="AR" term="%22Frappier%2C+Marc%22">Frappier, Marc</searchLink><relatesTo>1</relatesTo><i> marc.frappier@usherbrooke.ca</i><br /><searchLink fieldCode="AR" term="%22Mammar%2C+Amel%22">Mammar, Amel</searchLink><relatesTo>3</relatesTo><i> amel.mammar@telecom-sudparis.eu</i><br /><searchLink fieldCode="AR" term="%22Laleau%2C+Régine%22">Laleau, Régine</searchLink><relatesTo>2</relatesTo><i> laleau@u-pec.fr</i><br /><searchLink fieldCode="AR" term="%22Desharnais%2C+Jules%22">Desharnais, Jules</searchLink><relatesTo>4</relatesTo><i> Jules.Desharnais@ift.ulaval.ca</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Dec2016, Vol. 131, p76-93. 18p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22B+method+%28Computer+science%29%22">B method (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22ANSI+standards%22">ANSI standards</searchLink><br /><searchLink fieldCode="DE" term="%22Inconsistency+%28Logic%29%22">Inconsistency (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+notation%22">Mathematical notation</searchLink><br /><searchLink fieldCode="DE" term="%22Ad+hoc+computer+networks%22">Ad hoc computer networks</searchLink><br /><searchLink fieldCode="DE" term="%22Access+control%22">Access control</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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 FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=118898535
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.scico.2016.04.011
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 18
        StartPage: 76
    Subjects:
      – SubjectFull: B method (Computer science)
        Type: general
      – SubjectFull: ANSI standards
        Type: general
      – SubjectFull: Inconsistency (Logic)
        Type: general
      – SubjectFull: Mathematical notation
        Type: general
      – SubjectFull: Ad hoc computer networks
        Type: general
      – SubjectFull: Access control
        Type: general
    Titles:
      – TitleFull: A formal validation of the RBAC ANSI 2012 standard using B.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Huynh, Nghi
      – PersonEntity:
          Name:
            NameFull: Frappier, Marc
      – PersonEntity:
          Name:
            NameFull: Mammar, Amel
      – PersonEntity:
          Name:
            NameFull: Laleau, Régine
      – PersonEntity:
          Name:
            NameFull: Desharnais, Jules
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 12
              Text: Dec2016
              Type: published
              Y: 2016
          Identifiers:
            – Type: issn-print
              Value: 01676423
          Numbering:
            – Type: volume
              Value: 131
          Titles:
            – TitleFull: Science of Computer Programming
              Type: main
ResultId 1