1,721,126 research outputs found
Exploiting Probabilistic Trace Expressions for Decentralized Runtime Verification with Gaps
Full text linkMultiagent Systems (MASs) are distributed systems composed by autonomous, reactive, proactive, heterogeneous communicating entities. In order to dynamically verify the behavior of such complex systems, a decentralized solution able to scale with the number of agents is necessary. When, for physical, infrastructural, or legal reasons, the monitor is not able to observe all the events emitted by the MAS, gaps are generated. In this paper we present a runtime verification decentralized approach to handle observation gaps in a MAS
Protocols with exceptions, timeouts, and handlers: A uniform framework for monitoring fail-uncontrolled and ambient intelligence systems
No full textThis paper describes an approach for designing, formalizing and implementing sentinels that detect errors in fail-uncontrolled multiagent systems, and controllers that identify particular situations in ambient intelligence (AmI) systems. The formalism we use for representing the expected patterns of actions along with exceptions, timeouts, and their handlers, is that of constrained global types extended with features for dealing with these new constructs. We provide the syntax and semantics of the extended constrained global types and examples of their use, in the different contexts of fail-uncontrolled and AmI systems
Checked corecursive streams: Expressivity and completeness
No full textChecked corecursive streams are a novel approach to stream definitions relying on a semantics of function application detecting cyclic calls, and a well-definedness check ensuring that access to an arbitrary index will always return a result. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme. We show that this actually enhances expressive power, since the interleaving operator cannot be expressed by the others, and that it is still possible to perform a sound and complete well-definedness check, through a symbolic computation which mimics access to an arbitrary index
Enhancing Expressivity of Checked Corecursive Streams
No full textWe propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme
Runtime Verification of Hash Code in Mutable Classes
No full textMost mainstream object-oriented languages provide a notion of equality between objects which can be customized to be weaker than reference equality, and which is coupled with the customizable notion of object hash code. This feature is so pervasive in object-oriented code that incorrect redefinition or use of equality and hash code may have a serious impact on software reliability and safety. Despite redefinition of equality and hash code in mutable classes is unsafe, many widely used API libraries do that in Java and other similar languages. When objects of such classes are used as keys in hash tables, programs may exhibit unexpected and unpredictable behavior. In this paper we propose a runtime verification solution to avoid or at least mitigate this issue. Our proposal uses RML, a rewriting-based domain specific language for runtime verification which is independent from code instrumentation and the programming language used to develop the software to be verified
Flexible coinductive logic programming
No full textRecursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels
Exploiting Probabilistic Trace Expressions for Decentralized Runtime Verification with Gaps
No full textMultiagent Systems (MASs) are distributed systems composed by autonomous, reactive, proactive, heterogeneous communicating entities. In order to dynamically verify the behavior of such complex systems, a decentralized solution able to scale with the number of agents is necessary. When, for physical, infrastructural, or legal reasons, the monitor is not able to observe all the events emitted by the MAS, gaps are generated. In this paper we present a runtime verification decentralized approach to handle observation gaps in a MAS
Mind the Gap! Runtime Verification of Partially Observable MASs with Probabilistic Trace Expressions
No full textIn this paper we present the theory behind Probabilistic Trace Expressions (PTEs), an extension of Trace Expressions where types of events that can be observed by a monitor are associated with an observation probability. PTEs can be exploited for monitoring that agents in a MAS interact in compliance with an Agent Interaction Protocol (AIP) modeled as a PTE, even when the monitor realizes that an interaction took place in the MAS, but it was not correctly observed (“observation gap”). To this aim, we adapt an existing approach for runtime verification with state estimation, we present a semantics for PTEs that allows for the estimation of the probability to reach a given state, given a sequence of observations which may include observation gaps, we present a centralized implemented algorithm to dynamically verify the behavior of the MAS under monitoring and we discuss its potential and limitations
- …
