基于Object-Z与Markov链的校园卡系统测试用例

针对提高校园卡系统准确性和可靠性测试的要求,提出了Object-Z与Markov链结合的测试用例自动生成算法.使用Object-Z对系统进行形式化规约,生成测试场景和操作顺序图;将操作顺序图转换为Markov链使用模型;根据测试场景和Markov链使用模型生成数量相对合理的测试用例.该方法无需对系统进行运行,在需求分析与测试阶段就能对系统的功能进行测试.生成的校园卡系统测试用例证明该方法是有效的,并且在提高测试覆盖率的同时,使用Markov链也能保证对系统的可靠性测试.     

基于微分动态逻辑的CPS建模与属性验证

随着信息物理融合系统(Cyber-Physical Systems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Log-ic),其操作模型为hybrid program.将HybridUML模型转换为hybrid program时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybrid program对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.     

从UML状态图到PVS规范的自动转换、验证

将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS规范的转换模型与规则.     

Microsoft Query技术在PSMS二次开发中的应用

动力及环境集中监控系统(PSMS,Power and Surroundings Monitoring System)的用户在使用过程中,往往会结合自身维护实践的需要提出一些特定的需求,但监控产品厂家目前所提供的软件却又不足以支持这些功能.本文结合实例,介绍了如何充分利用Microsoft Query技术并结合结构化查询语言(SQL,Structured Query Language),自行定义报表,从动力监控系统的大型数据库中获取数据,自动生成报表的方法.实践证明该方法对于加强配线架的例行维护管理具有现实的重要意义.     

基于CCITTX.500的DIRECTORY系统开发

号码簿标准是CCITTX.500/ISO9594规定的在OS I环境下信息处理系统一个十分重要的标准.本文分析了符合标准的号码簿系统的基本要点;阐述了形式化描述技术ASN.1的实质以及为实现号码簿系统而建立的ASN.1协议开发环境的特点;从软件工程的角度描述了实现号码簿系统的软件的结构化设计思想;提出了几个值得考虑的问题.     

SAP-ERP系统的设计与实现之我见

本文首先分析企业需求,再根据企业需求进行系统功能设计和架构设计,实施针对企业客户需要的ERP系统二次开发.论文针对各模块给出了功能描述、流程设计和业务蓝图,并根据业务蓝图进行系统开发,开发语言为ABAP语言.开发过程主要使用了结构化程序设计的设计思路,结合了模块池、Report、Workbench等技术方式.最终通过实施ERP系统,实现了从采购、生产、设计、销售到财务整个产业链的优化整合,提升企业的管理.     

RFID网络中发现服务系统的一种形式化规约

本文针对EPCIS发现服务在大规模应用和数据安全方面的需求,基于"集中式索引"模式给出了EPCIS发现服务系统的一种体系结构.首先,使用TIOA语言从高层对整个系统基本功能进行了规约.然后,为了使系统在实际应用中负载均衡、具有高性能和可扩展性,又给出了一种基于Pub/Sub的多服务器分布式系统体系结构,并对该分布式系统的各个组成分别进行了规约.最后,本文基于"模拟关系"验证了该分布式系统满足(实现)了高层系统规约.     

一种基于B方法的网络发票系统设计与实现

目前,在软件项目设计方法中,B方法是少数几种能够贯穿从需求分析到系统实现环节的、对软件产品进行全生命周期管理的形式化方法之一。本文以网络发票系统为例,对其使用B方法进行产品设计的良好实践进行了说明,阐述了该方法从规格说明到精化、实现的实践过程。该过程使用Atelier B作为实现工具。     

一种度量软件需求的功能点方法

基于目前应用广泛的功能点分析方法,从软件需求规约的角度提出了合理度量面向对象系统的一系列映射规则和度量规则,解决了基于人工解释所导致的度量结果的不精确问题,并通过实例说明了这些规则的使用方法,具有较强的实用性.     

协同系统体系结构模型的形式化语义

 针对模型驱动的协同应用系统开发,将范畴理论、代数规范和进程代数相结合,为软件体系结构模型提出了一种新的语义描述方法.该方法在构件规约描述的基础上,用态射表示构件之间的关系,态射类型蕴含了构件关系的不同语义,从而用类型范畴图表来描述软件体系结构模型,用函子描述体系结构模型之间的映射关系.体系结构模型的形式化描述可用于判断一个转换是否满足某些特性或约束.以一个协同编著系统为例说明了该方法的应用.     

代码翻译在遗留系统改造中的应用

代码翻译可以实现程序在不同语言间的相互转换,是解决遗留系统语言陈旧问题的有效途径.针对基于NT平台的ASP/IIS站点向自主安全操作系统平台的移植需求,借鉴代码翻译的思想成功设计了ASP语言到PHP语言的脚本转换工具.该工具已经成功应用于大量站点样本的转换,不仅显著降低了平台移植的整体费用和时间,而且在新的操作系统平台上运行工作.     

自动信任协商的形式化描述与验证研究

首先提出了自动信任协商的通用形式化框架,并将典型的信任协商策略规约到上述框架内;其次,基于上述形式化框架对自动信任协商的形式化验证问题进行了定义,确定了形式化验证的目标以及一般流程;再次,研究了典型信任协商策略的形式化验证问题,讨论了相关问题的计算复杂性并得到系列结论;最后,利用逻辑编程方法和模型检测方法实现了自动信任协商的形式化验证。实验结果表明,规则数是影响形式化验证系统运行时间的关键因素,逻辑编程方法和模型检测方法在规则较少时效率较高,但逻辑编程方法的可扩展性不及模型检测方法。     

基于MC/DC准则的确认测试用例生成方法

形式化的需求规格说明以其能够被自动操纵的形式,精确地描述了软件预期提供的功能,为测试提供了良好的条件。运用模型检查技术自动生成测试用例是形式化方法在基于需求的测试中采用的主要途径。MC/DC(修改的条件/判定覆盖)准则是一种实用的软件结构覆盖率测试准则。结合模型检查技术,提出一种从形式化的软件需求中自动生成测试用例的方法,以达到对软件需求的类似于MC/DC准则的覆盖测试。以一个实际的案例为例,并检验其生成的用例对代码的覆盖率,证明方法的实用性。     

基于FPGA和ADV7123的红外图像显示卡的设计与实现

介绍了一种利用FPGA(现场可编程门阵列)和A/D转换芯片ADV7123实现红外图像显示卡的设计方法.该显示卡的主要功能包括像素灰度级转换、图像放大以及PAL(逐行倒相)制视频信号生成.详细讨论了显示卡的设计思想和硬件结构、FPGA各逻辑模块设计、FPGA配置加载、显示卡与主系统互连以及利用ADV7123生成PAL制视频信号的方法.该图像显示卡用于红外图像处理系统的硬件调试和红外图像处理算法的效果观测,实际使用情况表明,该显示卡能够很好地满足红外图像处理系统的图像输出需求.     

航空电子系统基于需求的自动测试方法

提出了一种基于需求的自动测试方法.该方法针对目前航空电子系统的系统设计与验证中的"V"型流程进行建模,并对其进行形式化的描述,以供计算机分析、识别.设计了一套有效、完备的自动测试系统以达到对系统需求的验证,并在此基础上提出了进一步研究的方向.通过实际软件验证了所提方法的有效性.     

从需求规约到软件体系结构——一个实例研究

软件需求工程和软件体系结构设计是软件开发中的两个早期关键活动．如何自动或半自动地实现从需求规约到软件体系结构的变换一直是学术界和产业界关注的难题．目前，实践中仍然没有系统化的、有效的方法、技术、工具和过程指导从需求规约到软件体系结构的变换．本文基于一个实际项目一奥运会注册制证子系统的软件体系结构建模，探讨了从需求规约到软件体系结构变换的经验性过程，并分析了变换过程中涉及的关键问题。以期为获得一个一般性变换过程奠定基础．     

嵌入式组态触摸屏与非标准通讯规约设备的一种通讯方法

目前很多电力电子装置采用非标准通讯规约,以至其无法直接与上位机通讯。文中介绍了一种嵌入式组态触摸屏与非标准通讯规约设备之间通讯的实现方法。该方法使用嵌入式组态软件提供的脚本驱动开发工具,编写非标准通讯规约的设备驱动,并将此设备驱动加载到嵌入式组态软件中,实现了两者之间的通讯。实际测试结果显示,使用该设备驱动,嵌入式组态触摸屏与非标准通讯规约设备之间通讯正常,遥测值读取准确,并且可以按照设定值定时刷新,遥调指令下发正确,从机设备可按照指令正确改变工作模式。     

面向计算机并发程序的形式化验证方法设计

计算机并发性程序形式化验证一直是软件安全领域的难题.软件并发性漏洞难以被发现,一旦发生问题,会造成不可估量的安全问题.形式化验证基于严格的数学推导基础,采用语言、语义、推理证明三位一体方法,构建形式逻辑系统,以确保被验证系统的安全性能.传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足,难以对计算机并发...     

一种VLSI设计到赋权超图的转换系统

本文基于VLSI划分问题的需要,提出了一种VLSI设计到赋权超图转换算法.该算法解决的关键问题是,它读取和遍历Verilog语言描述的树状结构VLSI设计,将其转换为赋权超图并存储为指定的文件存储格式,从而有效地将VLSI划分问题转换为超图划分优化问题.进而,本文给出了VLSI设计到赋权超图的转换系统（VLSI/Hypergraph Converter,VHC）的处理流程图,并在Windows平台下用C＋＋设计实现了VHC系统.实验及分析表明,该系统能正确地将Verilog语言描述的门级CPU测试用例转换为赋权超图,避免了直接在VLSI线网上进行划分,提高了VLSI划分的效率.     

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。