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!
Description
Summary: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.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2016.04.011