ﻻ يوجد ملخص باللغة العربية
Usage control models provide an integration of access control, digital rights, and trust management. To achieve this integration, usage control models support additional concepts such as attribute mutability and continuity of decision. However, these concepts may introduce an additional level of complexity to the underlying model, rendering its definition a cumbersome and prone to errors process. Applying a formal verification technique allows for a rigorous analysis of the interactions amongst the components, and thus for formal guarantees in respect of the correctness of a model. In this paper, we elaborate on a case study, where we express the high-level functional model of the UseCON usage control model in the TLA+ formal specification language, and verify its correctness for <=12 uses in both of its supporting authorisation models.
This paper presents two formal models of the Data Encryption Standard (DES), a first using the international standard LOTOS, and a second using the more recent process calculus LNT. Both models encode the DES in the style of asynchronous circuits, i.
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++,
We present a formal tool for verification of multivariate nonlinear inequalities. Our verification method is based on interval arithmetic with Taylor approximations. Our tool is implemented in the HOL Light proof assistant and it is capable to verify
The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However, computing and verifying approximations to the arctangent function are
We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several micro