the proceedings contain 20 papers. the special focus in this conference is on Invited talk, formal UML modeling, Components and architecture, Joint discotec session, Timed process algebra, Timed and hybrid automata, P...
ISBN:
(纸本)3642134637
the proceedings contain 20 papers. the special focus in this conference is on Invited talk, formal UML modeling, Components and architecture, Joint discotec session, Timed process algebra, Timed and hybrid automata, Program logics and analysis and Reasoning about distributedsystems. the topics include: formal software verification;exploiting the hierarchical structure of rule-based specifications for decision planning;reactive semantics for distributed UML activities;statistical abstraction and model-checking of large heterogeneous systems;formal semantics and analysis of behavioral AADL models in real-time maude;testing probabilistic distributedsystems;specification and testing of e-commerce agents described by using UIOLTSs;testing attribute-based transactions in SOC;grouping nodes in wireless sensor networks using coalitional game theory;forgetting the time in timed process algebra;theory and implementation of a real-time extension to the π-calculus;fuzzy-timed automata;model checking of hybrid systems using shallow synchronization;heap-dependent expressions in separation logic;on-the-fly trace generation and textual trace analysis and their pplications to the analysis of cryptographic protocols;on efficient models for model checking message-passing distributed protocols and logics for contravariant simulations
the proceedings contain 16 papers. the topics discussed include: a reversible abstract machine and its space overhead;a small model theorem for rectangular hybrid automata networks;analysis of may-happen-in-parallel i...
ISBN:
(纸本)9783642307928
the proceedings contain 16 papers. the topics discussed include: a reversible abstract machine and its space overhead;a small model theorem for rectangular hybrid automata networks;analysis of may-happen-in-parallel in concurrent objects;behavioural equivalences over migrating processes with timers;checking soundness of business processes compositionally using symbolic observation graphs;beyond lassos: complete SMT-based bounded model checking for timed automata;conformance testing of boolean programs with multiple faults;knowledge-baseddistributed conflict resolution for multiparty interactions and priorities;modelling probabilistic wireless networks;noninterference via symbolic execution;defining distances for all process semantics;secure multi-execution through static program transformation;and TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs.
distributed decentralized implementation of systems of communicating processes raises non-trivial problems. Correct execution of multiparty interactions, subject to priority rules, requires sophisticated mechanisms fo...
详细信息
Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based B...
详细信息
the proceedings contain 21 papers. the special focus in this conference is on formal techniques for distributedsystems. the topics include: Keep it small, keep it real: efficient run-time verification of web service ...
ISBN:
(纸本)3642021379
the proceedings contain 21 papers. the special focus in this conference is on formal techniques for distributedsystems. the topics include: Keep it small, keep it real: efficient run-time verification of web service compositions;approximated context-sensitive analysis for parameterized verification;verification of parameterized systems with combinations of abstract domains;on model-checking optimistic replication algorithms;a software platform for timed mobility and timed interaction;modeling, validation, and verification of PCEP using the IF language;distinguing non-deterministic timed finite state machines;system model-based definition of modeling language semantics;typing component-based communication systems;epistemic logic for the applied Pi calculus;on process algebraic proof methods for fault tolerant distributedsystems;using first-order logic to reason about submodule construction;a model-checking approach for service component architectures;dynamic symbolic execution of distributed concurrent objects;checking the conformance of orchestrations with respect to choreographies in web services;a type graph model for java programs and conformance testing of network simulators based on metamorphic testing technique.
object groups are collections of objects that perform collective work. We study a calculus withobject groups and develop a technique for the deadlock analysis of such systemsbased on abstract descriptions of method&...
详细信息
ISBN:
(纸本)9783642214615
object groups are collections of objects that perform collective work. We study a calculus withobject groups and develop a technique for the deadlock analysis of such systemsbased on abstract descriptions of method's behaviours.
In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this ...
详细信息
ISBN:
(纸本)9783642214615
In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this fact, and therefore may report it. Our approach uses knowledge properties that are precalculated based on model checking. As local knowledge is not always sufficient to monitor a global property in a concurrent system, we allow adding temporary synchronizations between two or more processes to achieve sufficient knowledge. Since synchronizations are expensive, we aim at minimizing their number using the knowledge analysis.
the proceedings contain 22 papers. the topics discussed include: on global types and multi-party sessions;linear-time and may-testing in a probabilistic reactive setting;a model-checking tool for families of services;...
ISBN:
(纸本)9783642214608
the proceedings contain 22 papers. the topics discussed include: on global types and multi-party sessions;linear-time and may-testing in a probabilistic reactive setting;a model-checking tool for families of services;partial order methods for statistical model checking and simulation;counterexample generation for markov chains using SMT-based bounded model checking;a framework for verifying data-centric protocols;relational concurrent refinement: timed refinement;Galois connections for flow algebras;an accurate type system for information flow in presence of arrays;analysis of deadlocks in object groups;monitoring distributedsystems using knowledge;global state estimates for distributedsystems;a process calculus for dynamic networks;and SimGrid MC: verification support for a multi-API simulation platform.
We consider distributedsystems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential subroutine for control, monitoring and diagnosis applications, we provide an algori...
详细信息
ISBN:
(纸本)9783642214615
We consider distributedsystems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential subroutine for control, monitoring and diagnosis applications, we provide an algorithm that computes, during the execution of the system, an estimate of the current global state of the distributed system for each local subsystem. this algorithm does not change the behavior of the system;each subsystem only computes and records a symbolic representation of the state estimates, and piggybacks some extra information to the messages sent to the other subsystems in order to refine their estimates. Our algorithm relies on the computation of reachable states. Since the reachability problem is undecidable in our model, we use abstract interpretation techniques to obtain regular overapproximations of the possible FIFO channel contents, and hence of the possible current global states. An implementation of this algorithm provides an empirical evaluation of our method.
Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been ...
详细信息
ISBN:
(纸本)9783642214615
Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms and communication protocol in the specification language TLA(+). In order to validate the model and to search for bugs we employed the TLA(+) model checker TLC to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA(+). A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.
暂无评论