A Valid and Correct-by-Construction Formal Specification of RBAC

2020 ◽  
Vol 14 (2) ◽  
pp. 41-61
Author(s):  
Hania Gadouche ◽  
Zoubeyr Farah ◽  
Abdelkamel Tari
Keyword(s):  
Formal Specification ◽  
Formal Method ◽  
A Priori ◽  
Critical Systems ◽  
Combinatorial Explosion ◽  
Access Control Models ◽  
Safety Critical Systems ◽  
Construction Specification ◽  
Access To Data ◽  
Abstraction Levels

Controlling access to data is one of the primary purposes of security, especially when it comes to dealing with safety critical systems. In such systems, it is of paramount importance to rigorously define access control models. In this article, a correct-by-construction specification of RBAC using the Event-B formal method is proposed. The specification defines closely the model properties with the behavior aspect of RBAC as guards of events, which allows applying a priori verifications. Accordingly, the resulted specification is correct-by-construction and avoids the combinatorial explosion problem. As well, a number of refinement operations are performed leading to a specification with several abstraction levels, where each level implements selected RBAC entities. The approach is illustrated by an instantiation of a healthcare system.

scholarly journals Learning from Demonstrations with High-Level Side Information

2017 ◽  
Author(s):  
Min Wen ◽  
Ivan Papusha ◽  
Ufuk Topcu
Keyword(s):  
Temporal Logic ◽  
Side Information ◽  
A Priori ◽  
Learning From Demonstration ◽  
Critical Systems ◽  
Learning From Demonstrations ◽  
Out Of Sample ◽  
Safety Critical Systems ◽  
Temporal Logic Formula ◽  
High Level

We consider the problem of learning from demonstration, where extra side information about the demonstration is encoded as a co-safe linear temporal logic formula. We address two known limitations of existing methods that do not account for such side information. First, the policies that result from existing methods, while matching the expected features or likelihood of the demonstrations, may still be in conflict with high-level objectives not explicit in the demonstration trajectories. Second, existing methods fail to provide a priori guarantees on the out-of-sample generalization performance with respect to such high-level goals. This lack of formal guarantees can prevent the application of learning from demonstration to safety- critical systems, especially when inference to state space regions with poor demonstration coverage is required. In this work, we show that side information, when explicitly taken into account, indeed improves the performance and safety of the learned policy with respect to task implementation. Moreover, we describe an automated procedure to systematically generate the features that encode side information expressed in temporal logic.

Generation of testing script based on XML for safety-critical systems

2011 ◽  
Vol 31 (1) ◽  
pp. 281-285
Author(s):  
Huan HE ◽  
Zhong-wei XU ◽  
Gang YU ◽  
Shi-yu YANG
Keyword(s):  
Critical Systems ◽  
Safety Critical ◽  
Safety Critical Systems
Sign in / Sign up

Export Citation Format

Share Document