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

Symposium of the South African Institute for Computer Scientists and Information Technologists (SAICSIT)

作者： Fourie, Jean Geldenhuys, Jaco Inggs, Cornelia Acuo Technol 35 Electron StrTechnopk Stellenbosch South Africa Stellenbosch Univ Comp Sci Div Dept Math Sci Stellenbosch South Africa

ISBN: (纸本)9781450313087

We examine the distributed breadth-first enumeration of a state space that is partitioned using a static partition function. Two of the key drawbacks of this approach are the high communication overhead and the excessive growth of the queues that hold states received from other nodes, ultimately resulting in memory exhaustion that causes premature termination of the distributed enumeration algorithm. This paper investigates a number of strategies to reduce communication times and queue lengths. Some aspects of the strategies are novel, including a local search technique, while others are standard techniques for reducing memory usage and time for both serial and parallel state enumeration algorithms. The queue reduction strategies effectively reduce the queue lengths and save memory, while the standard techniques outperform the other strategies in their effectiveness to reduce communication overhead.

关键词： distributed model checking Breadth-first search

来源：评论

学校读者我要写书评

暂无评论

distributed extended beam search for quantitative model checking

引用

4th International Workshop on model checking and Artificial Intelligence (MoChArt IV)

作者： Wijs, A. J. Lisser, B. CWI POB 94079 NL-1090 GB Amsterdam Netherlands

ISBN: (纸本)9783540741275

In this paper, we mainly focus on solving scheduling problems with model checking, where a finite number of entities needs to be processed as efficiently as possible, for instance by a machine. To solve these problems, we model them in untimed process algebra, where time is modelled using a special tick action. We propose a set of distributed state space explorations to find schedules for the modelled problems, building on the traditional notion of beam search. The basic approach is called distributed (detailed) beam search, which prunes parts of the state space while searching using an evaluation function in order to find near-optimal schedules in very large state spaces. Variations on this approach are presented, such as distributed flexible, distributed g-synchronised, and distributed priority beam search, which can also practically be used in combinations.

关键词： directed model checking distributed model checking scheduling beam search

来源：评论

学校读者我要写书评

暂无评论

dmcG: A distributed symbolic model checker based on GreatSPN

引用

28th International Conference on Applications and Theory of Petri Nets and Other models of Concurrency

作者： Hamez, Alexandre Kordon, Fabrice Thierry-Mieg, Yann Legond-Aubry, Fabrice Univ P&M Curie CNRS UMR 7606 LIP6 4 Pl Jussieu F-75252 Paris 05 France

ISBN: (纸本)9783540730934

We encountered some limits when using the GreatSPN model checker on life-size models, both in time and space complexity. Even when the exponential blow-up of state space size is adequately handled by the tool thanks to the use of a canonization function that allows to exploit system symmetries, time complexity becomes critical. Indeed the canonization procedure is computationally expensive, and verification time for a single property may exceed 2 days (without exhausting memory). Using the GreatSPN model-checking core, we have built a distributed model-checker, dmcG, to benefit from the aggregated resources of a cluster. We built this distributed version using a flexible software architecture dedicated to parallel and distributed model-checking, thus allowing full reuse of GreatSPN source code at a low development cost. We report performances on several specifications that show we reach the theoretical linear speedup w.r.t. the number of nodes. Furthermore, through intensive use of multi-threading, performances on multiprocessors architectures reach a speedup linear to the number of processors.

关键词： GreatSPN symbolic reachability graph distributed model checking

来源：评论

学校读者我要写书评

暂无评论

distributed Verification of Multi-threaded C++ Programs

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2008年第1期198卷 33-46页

作者： Edelkamp, Stefan Jabbar, Shahid Sulewski, Damian Univ Dortmund Dept Comp Sci Dortmund Germany

Verification of multi-threaded C++ programs poses three major challenges: the large number of states, states with huge sizes, and time intensive expansions of states. This paper presents our efforts in addressing these issues by combining an efficient use of hard disk with the distribution of the state space on several computing nodes. The approach is applicable to clusters and multi-core machines with single or multiple hard disks. We exploit the concept of a signature of a state that allows the full state vector to stay on secondary memory. For a distributed exploration of the state space, we report the lessons learned from using different partitioning schemes, including Holzmann and Bosnacki's [21] depth-slicing method, and their effects on blind and directed search algorithms. Empirical evaluation is done on our experimental C++ verification tool StEAM, which is capable of detecting errors such as segmentation faults, deadlocks, access conflicts, etc. The distributed algorithms are realized through MPI on a cluster of workstations.

关键词： Program Verification distributed model checking External model checking

来源：评论

学校读者我要写书评

暂无评论

Software model checking is a rich research field

引用

International Journal on Software Tools for Technology Transfer 2009年第1期11卷 1-11页

作者： Valmari, Antti Department of Software Systems Tampere University of Technology P.O. Box 553 33101 Tampere Finland

This introductory paper has been written for readers who know nothing about model checking but do know about software. Its aim is to present, almost without mathematical terms, the fundamental general approaches on which the papers in this Special Section build, and give an idea of what kind of contribution each paper makes. The main issues discussed are motivation for model checking, state spaces, and bounded model checking with sat solvers. Individual papers lead to discuss the following ideas: exploiting a distributed computing environment for model checking, constructing those states first that look most promising for eventually finding errors, only constructing a representative subset of states, the representation of contents of variables in an abstract way with approximation from below, and the use of more general solvers than sat solvers in bounded model checking. © Springer-Verlag 2008.

关键词： State space distributed model checking Directed model checking Partial-order methods Symbolic execution Bounded model checking Satisfiability

来源：评论

学校读者我要写书评

暂无评论

An Automated Translator for model checking Time Constrained Workflow Systems

An Automated Translator for Model Checking Time Constrained ...

引用

15th International Workshop on Formal Methods for Industrial Critical Systems

作者： Mashiyat, Ahmed Shah Rabbi, Fazle Wang, Hao MacCaull, Wendy St Francis Xavier Univ Ctr Log & Informat Antigonish NS B2G 1C0 Canada

ISBN: (纸本)9783642158971

Workflows have proven to be a useful conceptualization for the automation of business processes. While formal verification methods (e.g., model checking) can help ensure the reliability of workflow systems, the industrial uptake of such methods has been slow largely due to the effort involved in modeling and the memory required to verify complex systems. Incorporation of time constraints in such systems exacerbates the latter problem. We present an automated translator, YAWL2DVE-t, which takes as input a time constrained workflow model built with the graphical modeling tool YAWL, and outputs the model in DVE, the system specification language for the distributed LTL model checker DiViNE. The automated translator, together with the graphical editor and the distributed model checker, provides a method for rapid design, verification and refactoring of time constrained workflow systems. We present a realistic case study developed through collaboration with the local health authority.

关键词： Workflow Systems modeling Time Automated Translation distributed model checking

来源：评论

学校读者我要写书评

暂无评论

Reducing Time and/or Memory Consumption of The SOG construction in a Parallel Context 16

Reducing Time and/or Memory Consumption of The SOG construct...

引用

16th IEEE ISPA / 17th IEEE IUCC / 8th IEEE BDCloud / 11th IEEE SocialCom / 8th IEEE SustainCom

作者： Ouni, Hiba Klai, Kais Abid, Chiheb Ameur Zouari, Belhassen Univ Tunis El Manar Fac Sci Tunis Tunis 2092 Tunisia Univ Paris 13 CNRS UMR 7030 LIPNSorbonne Paris Cite Villetaneuse France Univ Carthage Higher Sch Commun Tunis Mediatron Lab Tunis Tunisia

ISBN: (纸本)9781728111414

An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). Such a graph is a condensed representation of the state space that is obtained by taking advantage of symbolic representation of the nodes. Each node, called aggregate, represents a set of explicit states and is encoded using Multi-valued decision diagrams. In a previous work, we have shown that parallel and distributed approaches can improve drastically the performances of the SOG computation regarding a sequential construction. In this paper, we go a step forward in improving the SOG construction process by reducing, on the fly, the size of its aggregates. We propose a Multi-valued decision diagrams (MDDs) based algorithm to determine a single representative for each strongly connected component in every aggregate allowing to remove from memory a consequent number of states which are no more necessary for the construction process. Two parallel approaches for the building of an SOG are proposed using such an optimization. The first approach is based on a shared memory architecture, while the second is based on a distributed memory one. The results of our preliminary experiments show that, in first case, the canonization allows to obtain more compact SOG (in terms of memory consumption) while increasing the computation time. However, for the distributed memory based approach, the canonization allows to reduce the size of exchanged messages and therefore reducing communication time.

关键词： Canonization distributed model checking Parallel model checking

来源：评论

学校读者我要写书评

暂无评论

Response property checking via distributed state space exploration 14

Response property checking via distributed state space explo...

引用

Conference on Formal Methods in Computer-Aided Design (FMCAD)

作者： Bingham, Brad Greenstreet, Mark Univ British Columbia Dept Comp Sci 201-2366 Main Mall Vancouver BC V6T 1Z4 Canada

ISBN: (纸本)9780983567844

A response property is a simple liveness property that, given state predicates p and q, asserts "whenever a p-state is visited, a q-state will be visited in the future". This paper presents an efficient and scalable implementation for explicitstate model of checking response properties on systems with strongly- and weakly-fair actions, using a network of machines. Our approach is a novel twist on the One-Way-Catch-Them-Young (OWCTY) algorithm. Although OWCTY has a worstcase time complexity of O(n(2) m) where n is the number of states of the model, and m is the number of fair actions, we show that in practice, the run-time is a very small multiple of n. This allows our approach to handle large models with a large number of fairness constraints. Our implementation builds upon PREACH, a distributed, explicit-state model checking tool. We demonstrate the effectiveness of our approach by applying it to several standard benchmarks on some real-world, proprietary, architectural models.

关键词： distributed model checking explicit-state model checking murphi liveness fairness

来源：评论

学校读者我要写书评

暂无评论

A State Space Distribution Policy Based on Abstract Interpretation

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第3期128卷 35-45页

作者： Orzan, Simona van de Pol, Jaco Espada, Miguel Valero CWI SEN 2 Amsterdam Netherlands

We aim at improving the performance of distributed algorithms for model checking and state space reduction. To this end, we introduce a new distribution policy of states over workers. This policy reduces the number of transitions between states located at different workers. This in turn is expected to reduce the communication costs of the distributed algorithms. The main idea is to use Abstract Interpretation techniques to compute a small approximation of the state space, starting from some high level description of the system. Based on this approximation, the connectivity of concrete states is predicted. This information is used to distribute states with expected connectivity to the same worker. Experiments show a considerable reduction of cross transitions, at the expense of a modest unbalance of nodes per worker.

关键词： distributed model checking Abstract Interpretation

来源：评论

学校读者我要写书评

暂无评论

distributed BDD-based BMC for the verification of multi-agent systems 10

Distributed BDD-based BMC for the verification of multi-agen...

引用

Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems: volume 1 - Volume 1

作者： Andrew V. Jones Alessio Lomuscio Imperial College London UK

ISBN: (纸本)9780982657119

We present a method of distributed model checking of multiagent systems specified by a branching-time temporal-epistemic logic. We introduce a serial algorithm, central to the distributed approach, for combining binary decision diagrams with bounded model checking. The algorithm is based on a notion of "seed states" to allow for state-space partitioning. Exploring individual partitions displays benefits arising from the verification of partial state-spaces. When verifying both an industrial model and a scalable benchmark scenario the serial bounded technique was found to be effective. Results for the distributed technique demonstrate that it out-performs the sequential approach for falsifiable formulae. Experimental data indicates that increasing the number of hosts improves verification efficiency.

关键词： distributed model checking bounded model checking binary decision diagrams verification of MAS

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：