Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTowards a Formal Model for Composable Container Systems
127
0
0.0
(
0
)
Added by
Marco Peressotti
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
In modern cloud-based architectures, containers play a central role: they provide powerful isolation mechanisms such that developers can focus on the logic and dependencies of applications while system administrators can focus on deployment and management issue. In this work, we propose a formal model for container-based systems, using the framework of Bigraphical Reactive Systems (BRSs). We first introduce local directed bigraphs, a graph-based formalism which allows us to deal with localized resources. Then, we define a signature for modelling containers and provide some examples of bigraphs modelling containers. These graphs can be analysed and manipulated using techniques from graph theory: properties about containers can be formalized as properties of the corresponding bigraphic representations. Moreover, it turns out that the composition of containers as performed by e.g. docker-compose, corresponds precisely to the composition of the corresponding bigraphs inside an ``environment bigraph which in turn is obtained directly from the YAML file used to define the composition of containers.
rate research
Read More
Cell injection is a technique in the domain of biological cell micro-manipulation for the delivery of small volumes of samples into the suspended or adherent cells. It has been widely applied in various areas, such as gene injection, in-vitro fertilization (IVF), intracytoplasmic sperm injection (ISCI) and drug development. However, the existing manual and semi-automated cell injection systems require lengthy training and suffer from high probability of contamination and low success rate. In the recently introduced fully automated cell injection systems, the injection force plays a vital role in the success of the process since even a tiny excessive force can destroy the membrane or tissue of the biological cell. Traditionally, the force control algorithms are analyzed using simulation, which is inherently non-exhaustive and incomplete in terms of detecting system failures. Moreover, the uncertainties in the system are generally ignored in the analysis. To overcome these limitations, we present a formal analysis methodology based on probabilistic model checking to analyze a robotic cell injection system utilizing the impedance force control algorithm. The proposed methodology, developed using the PRISM model checker, allowed to find a discrepancy in the algorithm, which was not found by any of the previous analysis using the traditional methods.
Program transformation has gained a wide interest since it is used for several purposes: altering semantics of a program, adding features to a program or performing optimizations. In this paper we focus on program transformations at the bytecode level. Because these transformations may introduce errors, our goal is to provide a formal way to verify the update and establish its correctness. The formal framework presented includes a definition of a formal semantics of updates which is the base of a static verification and a scheme based on Hoare triples and weakest precondition calculus to reason about behavioral aspects in bytecode transformation
This work presents a formal model that is part of our effort to construct a verified file system for Flash memory. To modularize the verification we factor out generic aspects into a common component that is inspired by the Linux Virtual Filesystem Switch (VFS) and provides POSIX compatible operations. It relies on an abstract specification of its internal interface to concrete file system implementations (AFS). We proved that preconditions of AFS are respected and that the state is kept consistent. The model can be made executable and mounted into the Linux directory tree using FUSE.
Trust and reputation models for distributed, collaborative systems have been studied and applied in several domains, in order to stimulate cooperation while preventing selfish and malicious behaviors. Nonetheless, such models have received less attention in the process of specifying and analyzing formally the functionalities of the systems mentioned above. The objective of this paper is to define a process algebraic framework for the modeling of systems that use (i) trust and reputation to govern the interactions among nodes, and (ii) communication models characterized by a high level of adaptiveness and flexibility. Hence, we propose a formalism for verifying, through model checking techniques, the robustness of these systems with respect to the typical attacks conducted against webs of trust.
There have been many proposals for access control models and authorization policy languages, which are used to inform the design of access control systems. Most, if not all, of these proposals impose restrictions on the implementation of access control systems, thereby limiting the type of authorization requests that can be processed or the structure of the authorization policies that can be specified. In this paper, we develop a formal characterization of the features of an access control model that imposes few restrictions of this nature. Our characterization is intended to be a generic framework for access control, from which we may derive access control models and reason about the properties of those models. In this paper, we consider the properties of monotonicity and completeness, the first being particularly important for attribute-based access control systems. XACML, an XML-based language and architecture for attribute-based access control, is neither monotonic nor complete. Using our framework, we define attribute-based access control models, in the style of XACML, that are, respectively, monotonic and complete.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
