基于细胞膜演算的Dryad形式化描述  

Formal description of Dryad based on membrane calculus

作　　者：刘磊[1] 刘丰[1] 任俊绮 吕帅[1,2] 

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]吉林大学数学学院,吉林长春130012

出　　处：《哈尔滨工程大学学报》2016年第11期1539-1545,共7页Journal of Harbin Engineering University

基　　金：国家自然科学基金项目(61300049;61402195;61502197);吉林省科技发展计划项目(20130206052GX;20140520069JH)

摘　　要：由于Dryad编程模型的实现并不开源,导致关于Dryad编程模型的理论研究较为缺乏。本文利用细胞膜演算在描述并发系统的优势,对Dryad编程模型中任务执行过程进行了准确清晰的形式化描述,并对Dryad编程模型的容错机制进行了描述,最后通过一个实例检验了形式化描述结果。本文的形式化描述方法有效地丰富了编程模型的理论体系,为编程人员提供了任务调度的优化依据,同时该形式化描述还可作为验证程序正确性的辅助工具。Because the dryad programming model is not an open-source model, conducting research on this model is relatively scarce. This study provides an accurate and explicit formal description for the task performance of the dryad programming model by utilizing the advantages of membrane calculus on the aspect of describing the concurrent system. This research also describes the fault-tolerant mechanism of the model. Accordingly, a real case is used to test the formalized description results. The formalized description method herein effectively enriches the theoretical system of the programming model. The method also provides a basis for the task scheduling optimization. Simul-taneously, the method can be used as an auxiliary tool to verify the program correctness.

关 键 词：云计算 编程模型 Dryad 细胞膜演算 形式化 有向无环图 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]