中文摘要：

由于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.