اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدDistributed System Contract Monitoring
58
0
0.0
(
0
)
تأليف
Adrian Francalanza Ph.D
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The use of behavioural contracts, to specify, regulate and verify systems, is particularly relevant to runtime monitoring of distributed systems. System distribution poses major challenges to contract monitoring, from monitoring-induced information leaks to computation load balancing, communication overheads and fault-tolerance. We present mDPi, a location-aware process calculus, for reasoning about monitoring of distributed systems. We define a family of Labelled Transition Systems for this calculus, which allow formal reasoning about different monitoring strategies at different levels of abstractions. We also illustrate the expressivity of the calculus by showing how contracts in a simple contract language can be synthesised into different mDPi monitors.
قيم البحث
اقرأ أيضاً
Cyber-Physical Systems~(CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, the spatial and temporal requirements play an es
sential role for their correct and safe execution. Furthermore, the local interactions among the system components result in global spatio-temporal emergent behaviors often impossible to predict at the design time. In this work, we pursue a complementary approach by introducing STREL a novel spatio-temporal logic that enables the specification of spatio-temporal requirements and their monitoring over the execution of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic with two novel spatial operators reach and escape from which is possible to derive other spatial modalities such as everywhere, somewhere and surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbours, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimisation. We prove that, for a subclass of models, all the spatial properties expressed with reach and escape, using euclidean distance, satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for STREL and, to demonstrate the feasibility of our approach, we show its application using the monitoring of a simulated mobile ad-hoc sensor network as running example.
With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs written in widely-used programming languages. However, deductive program v
erification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. In this paper, we present how we developed prototypal program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We added specification language constructs in a similar visual style, designed to make the intended semantics clear from the look and feel of the specification constructs. We provide support both for static and dynamic verification of Snap! programs. Special attention is given to the error messaging, to make this as intuitive as possible.
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) an
d breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coqs functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congresss behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.
Motor is the most widely used production equipment in industrial field. In order to realize the real-time state monitoring and multi-fault pre-diagnosis of three-phase motor, this paper presents a design of three-phase motor state monitoring and faul
t diagnosis system based on LabVIEW. The multi-dimensional vibration acceleration, rotational speed, temperature, current and voltage signals of the motor are collected with NI cDAQ acquisition equipment in real time and high speed. At the same time, the model of motor health state and fault state is established. The order analysis algorithm is used to analyze the data at an advanced level, and the diagnosis and classification of different fault types are realized. The system is equipped with multi-channel acquisition, display, analysis and storage. Combined with the current cloud transmission technology, we will back up the data to the cloud to be used by other terminals.
This paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that f
ormal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness of the problems that PCC addresses has already brought students to show interest in this project.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
