基于CCS的软件规范描述及实例研究

软件规范描述方法主要是软件工程化的UML方法与形式化方法二类方法。论文主要给出了基于CCS的软件规范描述,首先根据系统需求画出进程派生树和迁移图,再根据操作语义和系统约束条件得到进程表达式,并用Java语言实现了系统原型代码。笔者的工作证明了CCS具有细节化地描述系统内部状态,便于系统软件实现的能力;在手工转换进程迁移图到进程表达式的基础上,提出了自动转换的进一步研究思路。     

基于场景的联锁软件形式化模型生成方法

为保证列车运行安全和旅客生命财产安全,对车站联锁控制系统进行有效的分析、验证和测试是必不可少的,而形式化模型是联锁系统分析、验证和测试的基础.以计算机联锁软件的UML半形式化模型为基础,以事件确定有限自动机模型作为描述系统的形式化模型,研究UML2.0顺序图转换为事件确定有限自动机模型的方法.首先选取一组与交互行为相关的全局变量作为状态向量来分析和消解顺序图各个场景的消息以及不同场景间的同一消息的前后置状态向量值是否存在矛盾,从而得到一致性的需求场景;然后提取各对象的事件序列生成对应的事件确定有限自动机;最后通过组合系统中对象的自动机模型得到系统的事件确定有限自动机模型.该方法改善了安全苛求软件的设计与开发,为软件质量评估提供了技术支撑.     

OSI网络层：分析,描述,验证和实现

OSI网络层主要负责提供端开放系统间建立、维持和终止网络连接的手段,还提供通过网络连接进行数据交换的功能和过程方面的手段,按照合理的开发规范研制OSI网络层是本文的主题,它包括初始的分析、形式化描述、正确性验证和软件的实现等四个重要步骤:第一,初始的分析:精确理解ISO以及CCITT制定的有关国际标准,设计路由选择算法、流量控制算法和拥挤控制算法,同时考虑参数统计和故障诊断机构;第二,形式化描述:用SDL/GR工具和Petri网描述X.25分组级,用CHILL语言、状态转换图和时序图描述网络服务原语,第三,正确性验证:用矩阵代数方法和有限状态机器摄动分析法完成各规程的验证;第四,软件的实现:依照软件开发规范进行OSI网络层的软件设计、编码和调试。     

从形式化式样出发的实时控制软件开发

形式化语言能够对软件的功能进行精确的描述,在实时控制软件中引入形式化语言描述是必要的也是可能的本文介绍了形式化式样语言VDM-SL(Vienna Development Method-Specification Language),用VDM-SL给出了一个小型控制软件的形式化描述。基于形式化式样描述,提出了从形式化式样出发的控制软件开发最后就形式化语言应用于软件描述的前景进行了分析,同时指出了形式化语言和工具的不足。     

基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃,对于Web服务中的长、短事务进行形式化描述与验证是很重要的,但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法,采用重写逻辑工具Maude,对于描述Web事务的细胞膜演算,给出一个事务处理的通用框架,采用重写逻辑中的规则描述事务的具体活动,并且引入事务补偿机制刻画长事务的运行;并应用该模型形式化描述文中的Web事务经典例子,得到一个可执行的重写逻辑模型,便于以后采用Maude线性时序逻辑分析器进行形式化分析．     

微内核中断机制的形式化设计与验证

操作系统的正确性和安全性很难用定量的方法进行描述。形式化方法是操作系统设计和验证领域公认的标 准方法。以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证, 在自行开发的安全可信操作系统VTOS上加以实现,采用Isabelle/HOL对设计过程进行了形式化描述,对VTOS中 断机制的完整性进行了验证,这对操作系统的形式化设计和验证工作起到了一定的借鉴意义。     

构件式体系结构模型映射的形式化语义

语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的语义.体系结构模型的形式化语义用类型范畴图表来表示,态射合成被用来追踪构件模型之间的关联和映射,不同层次模型间的映射关系用态射和函子来形式化描述.以此为基础,进一步分析了模型转换应保持的语义特性.范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪.应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动开发提供了新的认知、设计和语义计算的指导架构.     

数字系统中高层次设计的最优调度算法比较

高层次设计技术是数字系统设计的关键技术，是近年来国内外研究、开发和应用的热门课题。文章用形式化方法描述了两种流行的高层次设计的软件算法，并进行了实验验证。     

一种B语言描述的需求模型到PIM的转换方法

MDA为软件的自动化构造提供了一种良好的途径,但是MDA更多地关注PIM到PSM的转换,却忽视了需求阶段对PIM精确性的影响。本文针对这种问题,首先对MDA的基本过程进行改进,提出对需求进行必要的形式化描述的思路,使得需求模型到PIM的转换变得更为容易,从而达到增强PIM精确性的目的;其次,通过对三种形式化语言的对比研究,发现B语言在需求模型的表示及转换方面具有优势,并结合例子展示了如何使用B语言对软件需求进行形式化描述;最后,本文结合模型转换框图,给出了B方法和类图的ecore元模型的图形化描述,进一步给出了用B语言描述的需求模型到PIM的基本转换规则,并借助JavaCC、JJTree和ATL插件等工具实现了需求模型到PIM的转换。     

面向对象分析到设计的类模型转换方法

面向对象方法中,类模型是一种描述分析和设计结果的重要的静态模型。由于所处空间的不同,分析阶段和设计阶段的类模型在表示类之间的关系等方面有一定的区别,作为对面向对象软件自动化方法的探讨,本文针对面向对象分析阶段和设计阶段所形成的类模型表示,给出了从前者到后者转换的一般方法,转换的结果能够直接用面向对象程序设计语言提供的机制来表述。     

工商所电子经济户口管理系统的分析与设计

工商所电子经济户口管理系统是一个典型的管理信息系统(MIS),其开发主要包括后台数据库的建立和维护以及前端应用程序的开发两个方面,对于前者要求建立起数据一致性和完整性强、数据安全性好的库,而对于后者则要求应用程序功能完备,易使用等特点.针对工商所事务管理的实际情况,利用Visual Foxpro6.0开发了该管理软件,文章较为详细地介绍了该软件的设计思想,特别是管理系统的设计方法与过程,对编制类似的管理软件有很好的实用价值.     

软件缺陷管理方案分析

基于作者软件开发和软件测试的工作经历,给出了一套软件缺陷管理方案,该方案对软件缺陷的管理内容和生命周期进行重点分析,定义了软件缺陷在其生命周期中的各个状态,以及状态之间的转换过程,然后在软件缺陷权利管理中给出了权限和角色分配方法,最后对方案提出了一些不足和改进。     

软件生命周期质量评价方法研究

针对软件质量现存评估标准一方面笼统抽象、主观性强,另外一方面缺乏对软件某个特定阶段质量评估模型的问题,通过对软件生命周期进行研究,对需求分析、软件设计、软件编码和软件测试四个阶段,从bug引入阶段、bug发现阶段、bug缺陷等级、bug数量、bug产生原因、bug修正代价六个方面进行分析,采用了改进加权模糊熵权法确定度量元权重系数,建立软件生命周期不同阶段质量评价模型及软件总体质量评价模型;通过工程实践结果证明,该生命周期质量评价模型能够有效地对软件不同阶段进行评价,为量化软件生命周期不同阶段质量水平提供了一种新方法,减少了软件质量评价中的主观性。     

基于Rational统一过程的合同管理系统分析与设计

目前软件项目呈现一种复杂性高、规模大的趋势,这给软件开发和软件升级带来了技术上和管理上的困难.Rational统一过程(RUP)通过循环的、可预测的方式对软件进行分析与设计.本文结合一个合同管理系统的开发,给出了这一开发方法的分析与设计过程,有效地解决了这类问题.     

Getting Software RITE

In traditional software development environments, many designers don't routinely put their software in front of users. If the ultimate measure of well-designed software is how effectively it serves its intended purpose, then validating that it does so is critical, and the sooner the better. Many user-centered design practitioners do this with usability testing. A formal usability test is a rather sciencey affair. It involves a number of different people in different roles. This paper deals with software design validation. This test-fix-test-fix cycle continues until the software starts to feel pretty tight. This approach is called RITE (Rapid Iterative Testing and Evaluation).     

基于生命周期的电力物资管理系统研究与实现

电力企业的生产就是围绕设备的运行、维护、检修、试验等工作展开。本文首先,采用生命周期管理理论,将它应用到电力公司物资管理过程具有重要意义。然后,做出物资全生命周期管理系统的需求分析,并且根据需求分析建立设备全生命周期管理系统。然后,根据全生命周期管理理论和方法,把电力物资信息管理分成五个阶段进行管理。并采用基子．NET框架,基于B／S架枸的实现方案对系统总体结构进行设计。最后,基于Microsoft Visual Studio 2005平台、SQL Server 2005数据库,对整个系统进行了具体实现。     

基于敏捷建模的形式化需求分析方法

软件需求分析是软件生命周期中最关键的一步。传统的需求建模方法主要有两个重大的缺陷：1）非形式化的需求描述常常导致需求的歧义性和不一致性,因而难以确认和验证;2）易变一牲,需求变更及其连锁反应是对项目质量、进度乃至合同履行影响最大的风险因素。本文针对软件需求分析阶段的难点,通过将形式化方法和敏捷建模理论相结合,提出一套基于敏捷建模的形式化需求分析方法。     

一种基于COM组件的可定制信息系统的设计与实现

通过分析当前一般信息系统的共性，在信息系统的生命周期内引入了系统内置工具的概念，改变了常规信息系统的软件体系结构，缩短了信息系统的开发周期，提高了信息系统的可扩展性和易维护性。在此基础上，提出了一种基于COM组件的可定制信息系统的设计方法及实现实例。     

业务流程管理与集成系统SynchroFLOW的软件体系结构

信息技术的快速发展和应用改变着企业的商业环境。面对市场竞争越来越激烈,如何提高系统柔性,以支持企业重组和业务流程再遣;如何集成异构系统,对原有系统资源的利用和保护。本文从业务域的角度提出了一种企业应用业务流程管理和集成系统SynchroFLOW的软件体系结构,该体系构架以企业业务需求的抽象与描述为基础,通过对企业应用业务流程、活动功能和活动参与者的信息交换机制的独立的封装,降低业务逻辑、业务数据和业务操作实体三者间的耦合,实现业务流程的柔性管理和异构环境下不同应用的功能集成。这样的系统不但具有较高的柔性和集成性,同时减轻需求确认和设计验证的难度和工作量,进而延长应用系统的生命周期。     

Specifying transaction-based information systems with regularexpressions

The work is about the formal specification of transaction-based, interactive information systems. A transaction is a task that the user can execute independently, and the system can be defined as a partially ordered set of transactions. The general framework is the transformational paradigm, based on the classical Waterfall development model (W.W. Royce, 1970). The stages are systems analysis, software specification, design, and implementation. The systems analysis and software specification stages are covered. An informal, transaction-oriented method for systems analysis is proposed. The resulting system specification involves two parts: a high-level specification of each transaction and a formal specification of the system's control flow, i.e., the order of execution of the transactions. The system's control flow is expressed in a formal language describing concurrent regular expressions built on transaction names. At the software specification stage, some operational requirements, such as connect/disconnect transactions and the application of the all-or-nothing principle, are added to the system specification. Then a serial product automaton (SPA) is used to transform the concurrent expression into a single regular expression. This result is proven to be consistent with the system specification