Relating trace refinement and linearizability
In the late 1980’s, Back extended the notion of stepwise refinement of sequential systems to concurrent systems. By doing so he provided a definition of what it means for a concurrent system to be correct with respect to an abstract (potentially ...
Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized ...
A verification and deployment approach for elastic component-based applications
Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed ...
Simulation relations for fault-tolerance
We present a formal characterization of fault-tolerant behaviors of computing systems via simulation relations. This formalization makes use of variations of standard simulation relations in order to compare the executions of a system that ...
Modeling and efficient verification of wireless ad hoc networks
Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of ...
Dynamic intransitive noninterference revisited
The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static ...