基于扩展CHAM的SA级路径覆盖方法

化学抽象机形式化语言（CHAM）通过把化学反应和抽象机的概念有机地结合来描述系统状态的变化,以此来指导分析和测试.针对软件体系结构（SA）中构件的概念,采用CHAM对SA中的构件进行建模,并据此导出该构件的标号迁移系统（LTS）,以表示该构件与其它构件之间的行为交互,并根据选取的测试覆盖准则,生成基于此构件的LTS中的所有测试路径.最后以B/S体系结构为例,通过实验验证了该方法在生成DB构件的测试路径上是可行的.     

利用硬件抽象机模拟执行技术设计JAVA处理器

提出了一个基于硬件抽象机的流水线微处理器设计框架,创造性地使用了一种基于标签结构的模拟执行技术.基于这一框架,描述了一个堆栈抽象机的工作原理,实现了一个Java指令级并行处理器.利用堆栈硬件抽象机和堆栈指令折叠技术的组合解决了Java处理器中的堆栈依赖瓶颈问题.软件模拟证明了该处理器能够最大限度地挖掘出Java程序中的指令级并行,并且拥有更高的处理能力.     

基于CHAM的SA级全路径覆盖方法

文中提出了通过CHAM描述的SA规格说明生成LTS,并根据测试需求进行测试覆盖准则的选取,然后利用全路径测试方法,生成基于此覆盖准则的测试路径.最后以B/ S结构为例,验证了该方法在生成SA级的测试路径上是可行的.     

Transputer阵列上的并行抽象机PAM／TGR性能评价

并行系统的性能评价对于完善系统和提高系统和提高生能具有重要作用。本文首先扼要地讨论并行系统中影响程序并行加速效果的因素，然后提出平均并行度 μａｖｅ的分析方法， 从理论上分析并行抽象机ＰＡＭ／ＴＧＲ所能开发的平均并行度，并与实测结果进行比较。其次讨论超越加速和病态加速两种在并行多机系统中可能出现的加速现象。在些基础之上，，基于典型的Ｂｅｎｃｈｍａｒｋ测试和评价并行图重写抽象机ＰＡＭ／ＴＧＲ的性能，最     

形式化方法B的证明技术

用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动持从规约到实现的全过程开发工作.本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性.     

应用基于抽象机的动态翻译设计Java处理器

本文提出了一种基于硬件抽象机的动态翻译技术,它可用于实现Java处理器.该技术采用了硬件抽象机的"模糊执行"(HAM)方法,通过分析Java程序之间的相关性,动态地将Java字节码转换成基于标签的类RISC指令.然后,将堆栈折叠与动态翻译相结合进一步优化指令.应用该技术设计了一个Java指令级并行处理器,并且扩展它,支持Java多线程功能.     

基于B方法的电梯控制系统形式化研究

B方法是一种新的形式化方法,使用B方法开发软件可有效提高软件的可靠性、可复用性和开发效率.文中使用B方法对电梯控制系统建立了抽象机模型并对其进行活性证明,自动生成相应软件,提高了电梯控制系统的可靠性和稳定性.     

并行推理机RAP/LOP-PIM及其优化并行编译器的设计与实现

本文重点论述并行推理机RAP/LOP-PIM及其优化并行编译器的设计与实现.首先,我们简要介绍并行执行模型RAP/LOP.然后给出基于RAP/LOP模型的并行抽象机和相应的体系结构.接着论述并行编译器的优化实现技术.最后通过模拟实验对系统性能进行了评估.