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

Incremental Parametric Development of Greedy Algorithms

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第SPEC. ISS.期185卷 47-62页

作者： Cansell, Dominique Mery, Dominique Univ Metz LORIA Ile Saulcy F-57045 Metz France Univ Nancy 1 LORIA F-54506 Vandoeuvre Les Nancy France

The event b method provides a general framework for modelling both data structures and algorithms. b models are validated by discharging proof obligations ensuring safety properties. We address the problem of development of greedy algorithms using the seminal work of S. Curtis;she has formalised greedy algorithms in a relational calculus and has provided a list of results ensuring optimality results. Our first contribution is a re-modelling of Curtis's results in the event b framework and a mechanical checking of theorems on greedy algorithms The second contribution is the reuse of the mathematical framework for developing greedy algorithms from event b models;since the resulting event b models are generic, we show how to instantiate generic event b models to derive specific greedy algorithms;generic event b developments help in managing proofs complexity. Consequently, we contribute to the design of a library of proof-based developed algorithms.

关键词： Formal method b event-based method refinement safety greedy algorithms

来源：评论

学校读者我要写书评

暂无评论

Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-based Development

Designing Old and New Distributed Algorithms by Replaying an...

引用

Seminar on Rigorous methods for Software Construction and Analysis

作者： Cansell, Dominique Meryl, Dominique Univ Metz LORIA Metz France Univ Henri Poincare Nancy1 LORIA Nancy France

ISBN: (纸本)9783642114465

The paper reports on practical experience with the event b method, when developing case studies, especially distributed algorithms, which are very complex to verify in practice. Using the event b method, we develop a famous distributed algorithm, namely the leader election protocol for an acyclic network, generally known as the IEEE 1394. The algorithm exists and the refinement helps us to model it entirely in an elegant way. The final model is very close to the real algorithm. Only the termination proof is missing, since it is a probabilistic algorithm, as well as the contention resolution, which is solved at a global abstract level. Modelling is clearly fundamental and complex;it should be carried out by persons able to use refinement and to manage abstractions or more precisely abstract models and proofs. Advantages of such an incremental development are multiple what we quote here and that will be explained in detail. We replay the development to improve the proof process and we obtain new distributed algorithms solving the leader election protocol problem. Two strategies are used to build the new algorithms;a first strategy is called the contention resolution;a second strategy is called the contention prevention and is based on a priority among possible nodes of the network. The two resulting algorithms are cheaper than the original IEEE 1394 protocol and neither acknowledgement, nor confirmation is required. We show how the techniques of localisation help in deriving the final distributed algorithm. The paper is an extended version of the complete development of the two new algorithms and it aims to emphasize methodological aspects related to the event 13 development.

关键词： Formal method b event-based method refinement safety proofs distributed systems

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：