检索结果-内蒙古大学图书馆

23rd Symposium on Formal Methods (FM)

作者： Bodeveix, Jean-Paul Brunel, Julien Chemouil, David Filali, Mamoun Univ Toulouse IRIT CNRS UPS Toulouse France Univ Toulouse ONERA DTIS Toulouse France

ISBN: (纸本)9783030309411;9783030309428

Chord is a protocol providing a scalable distributed hash table over an underlying peer-to-peer network. It is very popular due to its simplicity, performance and claimed correctness. However, the original version of the Chord maintenance protocol, presented with an informal proof of correctness, was since then shown to be in fact incorrect. It is actually tricky to come up with a provably-correct version as the protocol combines data structures, asynchronous communication, concurrency, and fault tolerance. Additionally, the correctness property amounts to a form of stabilization, a particular kind of liveness property. Previous work only addressed automated proofs of safety;and pen-and-paper, or automated but much bounded, proofs of stabilization. In this article, we report on the first mechanized proof of the liveness property for Chord. Furthermore, our proof addresses the full parameterized version of the protocol, weakens previously-devised invariants and operating assumptions, and is essentially automated (requiring limited effort when manual assistance is needed).

关键词： Chord Distributed protocol parameterized verification Liveness Stabilization proof

来源：评论

学校读者我要写书评

暂无评论

parameterized Analysis of Immediate Observation Petri Nets 40th

Parameterized Analysis of Immediate Observation Petri Nets

引用

40th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS)

作者： Esparza, Javier Raskin, Mikhail Weil-Kennedy, Chana Tech Univ Munich Munich Germany

ISBN: (纸本)9783030215712;9783030215705

We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE-complete, answering a question left open in a previous paper.

关键词： Petri nets Reachability analysis parameterized verification Population protocols

来源：评论

学校读者我要写书评

暂无评论

A Formal Specification and verification Framework for Timed Security Protocols

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2018年第8期44卷 725-746页

作者： Li, Li Sun, Jun Liu, Yang Sun, Meng Dong, Jin-Song Singapore Univ Technol & Design ISTD Singapore 487372 Singapore Nanyang Technol Univ Sch Comp Engn Singapore 639798 Singapore Peking Univ Sch Math Sci Beijing 100080 Peoples R China Natl Univ Singapore Sch Comp Singapore 487372 Singapore

Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols. A parameterized method is introduced in our framework to handle timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied pi-calculus as a formal language for specifying timed security protocols. It supports modeling of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.

关键词： Timed security protocol timed applied pi-calculus parameterized verification secrecy and authentication

来源：评论

学校读者我要写书评

暂无评论

Black Ninjas in the Dark: Formal Analysis of Population Protocols 18

Black Ninjas in the Dark: Formal Analysis of Population Prot...

引用

33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) held as part of the Federated Logic Conference (FLoC)

作者： Blondin, Michael Esparza, Javier Jaax, Stefan Kucera, Antonin Tech Univ Munich Fak Informat Garching Germany Masaryk Univ Fac Informat Brno Czech Republic

In this interactive paper, which you should preferably read connected to the Internet, the Black Ninjas introduce you to population protocols, a fundamental model of distributed computation, and to recent work by the ... 详细信息

ISBN: (纸本)9781450355834

关键词： population protocols distributed computing parameterized verification

来源：评论

学校读者我要写书评

暂无评论

PEREGRINE: A Tool for the Analysis of Population Protocols 30th

PEREGRINE: A Tool for the Analysis of Population Protocols

引用

30th International Conference on Computer-Aided verification (CAV) Held as Part of the Federated Logic Conference (FloC)

作者： Blondin, Michael Esparza, Javier Jaax, Stefan Tech Univ Munich Munich Germany

ISBN: (纸本)9783319961453;9783319961446

We introduce PEREGRINE, the first tool for the analysis and parameterized verification of population protocols. Population protocols are a model of computation very much studied by the distributed computing community, in which mobile anonymous agents interact stochastically to achieve a common task. PEREGRINE allows users to design protocols, to simulate them both manually and automatically, to gather statistics of properties such as convergence speed, and to verify correctness automatically. This paper describes the features of PEREGRINE and their implementation.

关键词： Population protocols Distributed computing parameterized verification Simulation

来源：评论

学校读者我要写书评

暂无评论

Lost in abstraction: Monotonicity in multi-threaded programs

引用

INFORMATION AND COMPUTATION 2017年 252卷 30-47页

作者： Kaiser, Alexander Kroening, Daniel Wahl, Thomas Univ Oxford Oxford England Northeastern Univ Boston MA 02115 USA

Monotonicity in concurrent systems stipulates that, in any global state, system actions remain executable when new processes are added to the state. This concept is both natural and useful: if every thread's memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unknown. In this paper, we show that finite-data thread abstractions for model checking can be at odds with monotonicity: predicate-abstracting monotone software can result in nonmonotone Boolean programs - the monotonicity is lost in the abstraction. As a result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties. This improves earlier approaches of enforcing monotonicity via overapproximations. We implemented our solution in the unbounded-thread model checker monabs and applied it to numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools. (C) 2016 Elsevier Inc. Allrightsreserved.

关键词： Multi-threaded software parameterized verification Monotonicity Predicate abstraction

来源：评论

学校读者我要写书评

暂无评论

Para: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms

引用

FORMAL METHODS IN SYSTEM DESIGN 2017年第2期51卷 270-307页

作者： Konnov, Igor Lazic, Marijana Veith, Helmut Widder, Josef TU Wien Vienna Univ Technol Inst Informat Syst E184 4 Favoritenstr 9-11 A-1040 Vienna Austria

Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: FTDAs have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm code is parameterized due to conditions counting the number of received messages. Recently, we introduced a technique that first applies data and counter abstraction and then runs bounded model checking (BMC). Given an FTDA, our technique computes an upper bound on the diameter of the system. This makes BMC complete for reachability properties: it always finds a counterexample, if there is an actual error. To verify state-of-the-art FTDAs, further improvement is needed. In contrast to encoding bounded executions of a counter system over an abstract finite domain in SAT, in this paper, we encode bounded executions over integer counters in SMT. In addition, we introduce a new form of reduction that exploits acceleration and the structure of the FTDAs. This aggressively prunes the execution space to be explored by the solver. In this way, we verified safety of seven FTDAs that were out of reach before.

关键词： parameterized verification Bounded model checking Completeness Partial orders in distributed systems Reduction Fault-tolerant distributed algorithms Byzantine faults

来源：评论

学校读者我要写书评

暂无评论

Lost in abstraction: Monotonicity in multi-threaded programs

Lost in abstraction: Monotonicity in multi-threaded programs

引用

25th Conference on Concurrency Theory (CONCUR) held jointly with the 9th International Symposium on Trustworthy Global Computing (TGC) / 8th International IFIP Conference on Theoretical Computer Science (IFIP-TCS)

作者： Kaiser, Alexander Kroening, Daniel Wahl, Thomas Univ Oxford Oxford England Northeastern Univ Boston MA 02115 USA

ISBN: (纸本)9783662445839

关键词： Multi-threaded software parameterized verification Monotonicity Predicate abstraction

来源：评论

学校读者我要写书评

暂无评论

Algorithmic verification of Component-based Systems

Algorithmic Verification of Component-based Systems

引用

作者： Qiang WANG ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE

学位级别：博士

This dissertation discusses algorithmic verification techniques for concurrent component- based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software/hardware system design in a rigorous and correct-by-construction manner. System design is defined as a formal, accountable and coherent process for deriving trustworthy and optimised implementations from high-level system models and the corresponding execution platform descriptions. The essential prop- erties of a system model are guaranteed at the earliest possible design phase, and a correct implementation is then automatically generated from the validated high-level system model through a sequence of property preserving model transformations, which progressively refines the model with details specific to the target execution platform. BIP comes with a well-defined formal modeling language and a toolchain to support the rigor- ous system design. The BIP modeling language offers a three-layered modeling mechanism, i. e. Behavior, Interaction, and Priority for constructing complex system behavior and architectures. Behavior is characterized by a set of components, which are formally defined as automata extended with local data variables. Interaction specifies the multiparty synchronization of components, among which data transfer may take place. Priority can be used to schedule the interactions or resolve conflicts when several interactions are enabled simultaneously. The key principle of this three-layered modeling mechanism is the separation of concerns, i. e. system behavior is captured by a set of components, and system coordination is modeled by interactions and priorities. In BIP, algorithmic verification techniques are applied to ensure the essential safety properties of the system designs. The first major contribution of this dissertation is an efficient safety verification technique for BIP system models

关键词： Component-based design Concurrent system Model checking Algorithmic verification parameterized verification Predicate abstraction Partial order reduction Symmetry reduction Well-structured transition system

来源：评论

学校读者我要写书评

暂无评论

Counting dynamically synchronizing processes

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2016年第5期18卷 517-534页

作者： Ganjei, Zeinab Rezine, Ahmed Eles, Petru Peng, Zebo Linkoping Univ Linkoping Sweden

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

关键词： parameterized verification Counting predicate Barrier synchronization Deadlock freedom Multithreaded programs Counter abstraction Predicate abstraction Constrained monotonic abstraction

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：