论文部分内容阅读
随着广域网络的发展和网络的可利用带宽的增长，以网络为中心的计算机辅助设计CAD环境—协同建模环境越来越显示其重要性。形式化方法是以数学为基础，来定义硬件系统和软件系统的规约，并对系统进行验证的语言、技术和工具。RAISE是形式化方法的一种，它的语言称为RSL。 规划控制下二阶段设计理论提出了一种对设计问题进行规划分解的有效的方法。规划利用面向对象的方法使工程设计问题变成了一个类层次结构，复杂的工程设计问题被分解成为简单的设计对象，分配不同的用户进行协同设计。 在类层次结构的环境下，通过对结点采用合理的加锁方法，解决协同设计并发的问题，实现系统的合理并行性，并可以保证整个系统的一致性。 作为国家863计划项目：“2001AA411320以成德绵为核心的区域现代集成制造系统开发及应用”与四川省重大科技攻关项目：“01GG010-01区域制造业信息化关键技术与应用研究”的一部分，本文对结点的加锁机制进行了详细的研究，并且用RAISE形式化方法进行了描述和实现，具体工作如下： (1) 分析和总结了协同设计系统各种并发控制机制及其优缺点； (2) 研究了协同设计系统中并发控制的加锁机制。指出加锁机制中各种锁的优缺点，引入多粒度加锁的机制，研究了多粒度加锁机制中各种锁的相互关系，指出了多粒度加锁机制的不足之处，并提出了解决方法； (3) 利用RAISE形式化方法对并发控制加锁机制进行描述，并完善了多粒度加锁机制； (4) 利用RAISE工具完成了加锁机制的验证和实现。