Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Formal Framework for Modeling Trust and Reputation in Collective Adaptive Systems
92
0
0.0
(
0
)
Added by
EPTCS
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Authors
Alessandro Aldini
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
Collective Adaptive Systems (CAS) consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour that may be competing for shared resources even when collaborating to reach common goals. It is important to carry out thorough quantitative modelling and analysis and verification of their design to investigate all aspects of their behaviour before they are put into operation. This requires combinations of formal methods and applied mathematics which moreover scale to large-scale CAS. The primary goal of FORECAST is to raise awareness in the software engineering and formal methods communities of the particularities of CAS and the design and control problems which they bring.
We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labeled Transition Systems that are also used to define bisimilarity between components. Labeled bisimilarity is in full agreement with a barbed congruence, defined by simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.
The salient features of blockchain, such as decentralisation and transparency, have allowed the development of Decentralised Trust and Reputation Management Systems (DTRMS), which mainly aim to quantitatively assess the trustworthiness of the network participants and help to protect the network from adversaries. In the literature, proposals of DTRMS have been applied to various Cyber-physical Systems (CPS) applications, including supply chains, smart cities and distributed energy trading. In this chapter, we outline the building blocks of a generic DTRMS and discuss how it can benefit from blockchain. To highlight the significance of DTRMS, we present the state-of-the-art of DTRMS in various field of CPS applications. In addition, we also outline challenges and future directions in developing DTRMS for CPS.
In this extended abstract a view on the role of Formal Methods in System Engineering is briefly presented. Then two examples of useful analysis techniques based on solid mathematical theories are discussed as well as the software tools which have been built for supporting such techniques. The first technique is Scalable Approximated Population DTMC Model-checking. The second one is Spatial Model-checking for Closure Spaces. Both techniques have been developed in the context of the EU funded project QUANTICOL.
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
