摘要：传统的硬件验证方法将RTL设计综合成门级网表并使用SAT求解器进行验证,没有有效利用其字级结构,导致部分性质不能验证。近年来,软件分析验证技术和SMT求解技术取得了长足的发展,为将最新的软件分析验证技术迁移到硬件验证上来,提出一种基于C语言程序分析验证技术的Verilog代码验证方法。首先设计一个基于综合语义的Verilog到C的转换系统;然后使用当前软件分析验证领域典型的技术与工具对转换后的C语言程序进行分析验证,以判定原Verilog代码是否满足性质断言。实验结果表明了将C语言程序分析验证技术迁移到Verilog代码验证上的可行性和有效性。

摘要：软件在国民经济和社会生活中发挥着重要作用.软件出现故障给人们的工作、生活带来不便,甚至造成严重危害.但是当前所进行的多为软件故障诊断中单项活动的研究,较少有对各项诊断活动及其相应方法进行有效集成的研究.文中分析软件失效机理和软件故障产生原因,讨论软件故障模型,提出一种由故障检测、故障定位、故障排除、交付等组成的集成化的软件故障诊断过程框架,研究软件故障检测、定位和排除中所采用的方法及相应的过程,并且将该框架应用于实际的软件故障诊断.

摘要：nH-PROLOG,SPRF 和 N-PROLOG 是 PROLOG 的三种典型扩充,本文介绍了它们之间的异同。这三个系统采用不向方法扩充了 PROLOG,但是均使用情况分析法做为非 Horn 推理机制尽管它们的出发点、目的、表达形式各异,但在使用情况分析法这一点上有着惊人的相似性,这说明它们的推理在本质上是—般的和直观的。它们的区别在于:一个系统的性质要加入另一系统,必须做较大的变形。

摘要：近年来,越来越多的以计算机网络为平台的应用系统表现出自主性、动态性、开放性和异构性的特点,这使得软件开发理论和技术需要从软件体系结构的角度对这类系统的开发提供支持.面向Agent的软件开发技术提供了高层和自然的抽象方式对软件系统进行分析和设计,但现有面向Agent的方法学将Agent Class或者Agent Type视为多Agent系统软件体系结构的软构件,与Agent之间的关系仅仅是实例化的关系,这难以满足复杂系统对动态性的需求.从软件体系结构的角度上分析了多Agent系统中软构件的形式和机制,将Caste作为软构件,并以此为基础提出了Caste与Agent之间的动态绑定关系,定义了支持该机制的4个基本操作join,quit,activate和inactivate及其操作语义,用以来指导多Agent系统软件体系结构的设计和实现.

摘要：瑞吉欧马拉古兹研究中心的幼儿园认为,任何一个幼儿园环境设计首要的、也是最重要的是为儿童的未来创设生活的空间。环境是帮助幼儿成长的第一位教师。马拉古兹研究中心幼儿园的环境从内部空间的设计到家具,玩具和材料所体现的理念是一致的。

摘要：统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.

摘要：面向对象方法学已经越来越引起人们的重视。人们从程序设计、软件设计、软件开发等方面对它进行了研究。本文着重从软件开发的角度,分析了面向对象方法学的特点。然后介绍了面向对象的软件开发方法OOSDM,这种开发方法将面向对象的思想贯穿于始终。采用多视点的方法分析问题,解决问题。最后重点介绍了我们在OOSDM中采用的需求分析方法OORAM 及其支持工具。

摘要：自适应系统具有环境开放性、变化敏感性、系统动态性等复杂性特点,如何支持这类复杂系统的开发和维护是目前软件工程关注的焦点.将自适应系统中的自主运行单元抽象为软件Agent,借助组织学思想提出了支持自适应系统运行的动态绑定机制,设计了表述Agent如何适应环境变化的自适应策略描述语言SADL(self-adaptive strategy description language),开发了SADL的编译器和运行支撑环境.该方法将复杂自适应系统的自适应逻辑和业务逻辑相分离,通过SADL语言显式地描述系统的自适应特征,从而简化了复杂自适应系统的开发和维护.通过案例分析,阐述了如何基于上述方法来进行复杂自适应系统的开发,验证了方法的有效性.

摘要：随着软硬件系统复杂性的不断提高,各种验证技术被越来越广泛的使用.模型检验技术是一种保证软硬件设计、实现正确性的有效技术.在针对软硬件的模型验证技术中,一般采用时序逻辑作为规约语言.模态μ-演算是模态和时序逻辑中应用较为广泛的一种,它具有语法成分简洁、表达能力强等特点.扩展了Lange和Stirling基于Focus Game的LTL和CTL的公理化方法.提出了一种基于Game理论的μ-演算公式的可满足性的测试方法,该种方法能够将模态μ-演算公式的可满足性问题转化为FocusGame的求解问题.进一步,基于这套Game规则,给出了一个新的关于μ-演算可靠完备的推理系统.同已有的μ-演算公理系统相比,该推理系统相对直观、简洁.

摘要：针对智能化软件分析方向的人才培养要求,系统调研国内外一流高校相关课程教学情况,提出基础理论、关键技术、典型应用三层结构的智能化软件分析原理课程内容组织架构,并在课程实施、理论讲授和成绩考核等方面采取一些改革措施,取得了较好的教学效果。