示范性软件学院验收评估的思考与体会

我应邀参加了2003年9月教育部和软件行业协会组织的示范性软件学院的中期评估和2006年5月示范性软件学院的验收活动。两次活动我去的学校都相同。它们是:北京大学、华东师范大学、复旦大学、上海交通大学、同济大学和浙江大学(即下文指的六所软件学院)。我目睹和感受了这六所大学示范性软件学院的创业者们以改革、创新的精神培养新型软件人才所取得的成就。它们在办学指导思想、办学模式、教育教学改革、教师队伍建设、办学条件、学生工作、毕业生就业等方面都取得了可喜的成绩。本期《计算机教育》杂志集中报道这方面的情况,借此机会谈谈我的感受和体会,由于时间和篇幅的限制不可能很全面。     

基于MYGCC的编程规则检查算法研究

MYGCC是一个编程规则检查工具,其目前的检查算法存在局限性,不能完整地展示违反编程规则的程序路径。本文提出并实现了一种改进的编程规则检查算法,可以弥补上述的局限性。实验表明改进算法是有效的,此改进有助于用户更准确地定位错误位置,方便对编程错误的修正。     

从应用的角度评估MAS体系结构风格

近年来,Agent技术已成为开发复杂系统的一项可行技术,但对MAS体系结构的研究仍然面临着一定的挑战。本文从已有的MAS体系结构风格和开发框架出发,对MAS体系结构风格进行了分析、提取和归类,从应用角度提出了一个评估MAS体系结构风格的框架,并通过两个案例说明了如何利用评估结果为具体应用选择合适的风格。     

软件可靠性工程框架和评估系统实现

给出了软件可靠性工程的实施框架,它规范了软件可靠性评估的过程.文章还提出一个软件可靠性评估系统的体系结构,并给出了实现所需要的一些关键技术.已经依此实现了一个软件可靠性评估系统CaSoR(Computer aid Software of Reliability),并已经被实际     

基于LSC的模型检验研究

LSC是一种表达能力很强的顺序图建模语言,模型检验技术是验证软件模型正确性的重要方法,提出了一个对LSC模型进行模型检验的方法,并实现了相关支持工具。首先分析了LSC语言,然后基于其语义提出了生成LSC等价状态模型的方法,进而对生成的状态模型进行模型检验;最后进行了实例研究,利用给出的实现工具检验了用CTL描述的验证性质。     

一种基于抽象解释的WCET自动分析工具

利用基于抽象解释的变量值范围传播技术,提出了一种自动分析高级语言程序流信息的方法;并在白盒测试工具NPCA的基础上,利用该方法实现了WCET分析工具NPCA-WCET。     

面向路径的测试数据自动生成工具及其图形界面的Tcl/Tk设计

面向路径的测试数据生成问题是软件测试中一个基本问题。文章介绍了自主开发的面向路径的测试数据自动生成工具。Tcl/Tk是一种图形界面设计工具,其功能强大,可运行于Windows,UNIX等操作系统上,具有良好的可移植性。文章简要介绍Tcl/Tk,并给出用Tcl/Tk设计面向路径的测试数据自动生成工具的图形界面的方法。     

面向路径的测试数据自动生成工具的设计与实现

面向路径的测试数据生成问题是软件测试中的一个基本问题。Gupta等提出一种线性化谓词函数的迭代松驰方法求解该问题。文献[2]改进了该方法，证明改进后的方法与原方法生成的约束系统相同，文章以改进后的方法为核心算法，根据软件工程的思想，采用面向对象的方法，使用UML进行设计，并且在Linux Red Hat7.0操作系统下用C＋＋语言言实现一个为程序路径自动生成测试数据的原型工具，然后将它移植到Windows操作系统。     

多Agent系统中软构件的动态绑定机制及其操作语义

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

UML Statecharts的切片模型检验方法

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