组件语义约束的动态模型检测方法和技术研究
文献类型：学位论文
| 作者 | 倪彬 |
| 学位类别 | 博士 |
| 答辩日期 | 1998 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 组件 语义约束 模型检查 动态检测 规范 组合软件开发方法 |
| 学位专业 | 计算机软件 |
| 中文摘要 | 随着网络技术的发展，特别是因特网（Internet）的应用，信息系统的规模不断扩大，网络计算（Network Computing）模型成为主流，系统结构逐渐演化为三层客户/服务器结构。如何开发基于网络计算模型和三层结构的大规模应用软件是目前学术界和工业界共同关注的问题。另一方面，对象技术是当今软件工程发展的主流技术。在对象技术的基础上，组合软件开发方法和技术正在成为支持网络计算模型和三层客户/服务器结构的一种热点方法。可复用的组件是组合软件开发方法的基本单元和核心。组件的规范和实现通常依据一定的标准。组件标准提供了支持组件构造的系统结构和API。但是，这些标准目前都采用非形式的方法来刻画组件的语义。组件的高质量是复用和支持分布式计算的关键。为了开发高质量的组件，我们希望对组件的语义进行形式化地描述和验证。在很多情况下，这样的描述和验证是必要的。在组件的制造过程中，往往需要进行多层次的分析、设计和实现。组件语义精确和严格的形式描述，使各层次开发人员对组件语义不会产生理解上的歧义。对组件、调整组件、组合构造以及系统进化的重要依据和正确性检验手段。我们选定Java Beans组件标准作为研究的具体对象。论文工作主要包括下面几个方面的内容：1）设计了一个形式化的规范语言JBDL（Java Beans Description Language）来刻画Java Beans组件－－Bean的语义约束。JBDL是基于多类一阶谓词分支时序逻辑的描述语言，包括四种约束。静态约束刻画了Bean的状态空间。行为约束刻画了Bean各个操作应该满足的前后条件。生命期约束刻画了Bean在创建之后，由事件驱动的整个生命期过程中自身状态和行为应该满足的时序性质。协作约束刻画了由低层Bean协作完成高层Bean的操作时应该满足的时序性质。JBDL语言设计的创新特色及所解决的关键技术难点是：（1）单个Bean语义和协作语义的统一约束。（2）用以支持表达Java Beans对象特性的逻辑语言扩充。（3）用以支持统一地、混合地表达Bean状态和操作时序关系的逻辑语言语义上的扩充。JBDL具有较强的表达能力。它全面地描述了Bean的语义约束，统一地约束了单个Bean的语义和协作的语义。为完备地、严格地规范Bean提供了必要条件。对支持组合软件开发过程，特别是组合构造的过程，以及支持组件的复用和提高组件的质量都具有重要的意义。2)为了检测Bean的JBDL规范与其实现的一致性，我们提出了一种基于抽象和符号化的动态模型检查方法。这种方法通过在Bean的运行过程中，动态地建立和演化Bean的检测模型，并对该模型的抽象和符号化表示进行模型检查来完成一致性检测的任务。动态模型检查方法的创新特色及所解决的关键技术难点是：（1）模型的建立、演化以及检测的进行。我们设计了检测点事件机制、检测点选取策略和检测Bean生成方案，使得待检测Bean在运行过程度中需要被检测的时候能够激发检测点事件，也使得根据JBDL规范生成的检测Bean能够在检测点事件驱动下建立、演化检测模型，并进行检测。（2）时序公式的三值语义。由于检测模型是不断演化扩充的，在一个检测点某些时序公式的值按照JBDL的语义虽然是为假，但随着检测的继续，在进一步演化后的检测模型上它们的值可能为真。这就要求我们区分两种情况，a）公式目前不满足，但随着检测模型的演化，公式可能在将来满足；b）公式在从现在开始的检测模型上不可能满足，我们把第一种情况下公式的值定义为不确定（unknown）。这样，时序公式在检测模型下的语义就有三种取值。针对这个问题，我们给出了JBDL时序公式在检测模型下的三值语义解释。（3）空间耗尽问题。由于Bean每个状态占用的空间较多，同时状态数目在动态检测中不断增长，直接在检测模型上进行模型检查很容易空间耗尽。为此，我们提出了一种基于抽象划分的模型检查方法。特别地，抽象是根据要检测的约束而来的，避免了在抽象空间上进行操作和谓词的抽象计算。抽象模型的每个状态只需用布尔向量来表达，同时总的状态数目是有限的。这样，空间耗尽的问题可以通过直接构造抽象模型来有效解决。（4）抽象的保守性。保守性要求检测模型上能够检测到的错误一定可以在抽象模型上检测到。根据时序公式的三值语义，我们证明了抽象方法对正时序公式是保守性的。（5）模型检查算法。利用BDD进行符号化的表示可以提高模型检查的有效性。为了能够在抽象模型上对具有三值语义的时序公式进行模型检查，我们对BDD进行了扩充。使用T~3BDD对抽象模型和约束公式进行符号化的表示。同时给出了基于T~3BDD的模型检查算法，提高了检测的有效性。（6）对并发的影响。Bean通过多线程实现了多层次的并发。我们的动态检测方法给出了同步控制策略，使得检测对Bean的并发活动--特别是同步活动不产生影响或尽量少地产生影响。（7）自动检测。我们的抽象方法和模型检测方法支持检测Bean的自动生成，同时检测点事件包装也可以自动完成，因此检测可以自动地进行。一致性检测的方法是形式化模型检查和软件测试相结合的方法，使得检测可以机械和自动的进行。检测中动态建摸有效地支持了Bean独立发布的特性。时序公式的三值语义适应了检测模型的动态演化。基于抽象的模型检查有效地解决了检测中空间耗尽的问题。保证了正时序公式的保守性。T~3BDD的使用提高了模型检查的效率和有效性。动态检测方法也是基于状态的检测和基于外部行为的检测相结合的方法，支持检测Bean的并发特性和容错特性。它通过检测点机制提供了全局的、外挂的检测方案。也为Bean的测试结果提供了预言。整个方法自动化程度高，具有较好的实用性。3）根据JBDL规范和动态模型检查方法，我们设计和实现了检测的支撑框架和工具--MChecker。检测方法支撑框架是通过Java Beans的类实现的，包括检测点事件支撑框架，T~3BDD支撑框架，模型检查支撑框架和动态检测支撑框架。MChecker的工具包含检测Bean自动生成器和检测点事件包装器。利用MChecker，我们对JavaSoft提供的分布对象计算实例--股票报价监测器，和动画实例--杂耍者进行了研究。实验结果与理论结果完全一致，表明了动态检测在时间和空间上都是有效的。如何在虚拟机的层次上进行检测；如何把检测方法运用于分析、设计等高层次的开发阶段；如何把检测方法应用于其他的组件标准；如何从规范生成测试用例是值得进一步研究的几个方面。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 123 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6348]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 倪彬. 组件语义约束的动态模型检测方法和技术研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。