使用SPEC#开发高可靠性的算法程序

概要介绍了SPEC#的基本特性;使用SPEC#开发了若干典型的算法程序,利用该语言中的契约机制来形式化地描述前置条件、后置条件、对象不变式等程序规约,从而显著地提高了程序的可读性、可靠性和可维护性,有助于软件自动化水平的提高。     

一种描述安全协议的形式化规范语言

安全协议的设计和分析是复杂而且容易出错的。使用形式化的语言有利于安全协议的正确性和完整性。现有的安全协议的描述方法大多很复杂而且容易导致二义，从而导致协议隐含着种种的安全隐患。引入了基于构造类别代数的形式化规范语言来规范安全协议，通过规则集合和公理集合对安全协议进行精确地描述，有利于协议设计地规范化和协议漏洞地发现，同时对Needham-Sehroeder协议进行了形式化规范以进一步说明该形式化语言地使用。     

基于B语言的UML形式化方法

分析了目前主要的UML形式化方法及特点，提出了基于B语言的转换方法B2F(B-Based Formalization)，通过将UML模型转化为B抽象机描述实现UML的形式化描述和验证，并详细分析了基于B2F方法的UML类图的形式化，证明了该方法的可行性。     

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

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

轨道交通联锁领域特定语言的形式化

作为轨道交通系统的核心子系统之一，对联锁系统进行形式化建模与分析，是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合，由于形式化知识难以掌握，领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题，针对联锁系统的故障随机性、行为实时性、构件可重用的特点，提出设计联锁领域特定语言IS-SDL描述具体的联锁系统的参数，并基于随机混成自动机模板自动生成联锁系统的形式化模型，以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析，根据不同案例设计其领域特定语言；其次，确定联锁系统的系统模型的模板，包括环境构件模板和控制器模板，并举例抽取其随机混成自动机模板；在模板基础上定义系统模型生成过程，让领域专家可以通过领域特定语言，输入参数自动生成具体的随机混成自动机系统模型；最后以某站联锁系统为例，展示了基于模板的具体系统模型的生成过程，并通过基于系统模型的事故预测分析，证明了该方法的可行性与有效性.     

XQuery语言的形式化语义

XQuery语言用于查询XML文档。目前，该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化，本文通过重用XML家族语言通用语义构件的方法，形式化建模XQuery语言的语义，语义的描述采用Object—Z规范语言。这种面向对象的语义描述不仅具有简洁性、可扩展性和可组合性，而且有助于规范之间的一致性和协调性。     

基于Petri网的WSCI形式化模型分析

WSCI是一种Web服务组合标记语言,对于一些关键的业务流程,任何设计错误都会造成重大损失,因此有必要为WSCI语言建立形式化模型并给予分析,从而保证正确的业务流程部署。本文主要给出了WSCI的分析方法,基于文献[1]给出了形式化模型,提出了该形式化模型下的一种网融合方法。该方法将表示进程的网模型与其表示例外处理和子流程的网模型进行合并,形成统一的网模型。本文最后还给出了在该网模型下的可达图分析方法,从而达到分析带有例外处理的WSCI形式化模型的目的。     

一种面向嵌入式实时软件的需求建模语言

针对嵌入式实时系统复杂动态交互行为和严格实时的领域特征，提出了一种软件需求规约语言RTRSM。该语言以扩充的层次并发有穷状态机HCA为核心，以支持合成的模板为基本组成单元．利用转换有效期和事件预定机制来描述时间限制，既具有较强的时间限制描述能力，又能自然而直接地支持交互行为的建模，可执行且具有良好的形式语义。给出了该语言的形式化语法，举例说明了其时间描述机制，并通过执行步算法和基于HCA项的结构化操作规则定义了该语言的形式化操作语义。     

AspectualACME语言切点指示器的形式化描述方法

面向方面软件体系结构描述语言AspectualACME虽引入了切点指示器PCD(Pointcut Designator)的语法成分,但仍未给出其语义的形式化描述。针对这一问题,基于AspectualACME语言抽象语法树,设计了一阶逻辑语言LIAPCD(Logic Language forPCD)。在此基础上提出了AspectualACME语言PCD的形式化描述方法。该方法能精确定义软件体系结构层PCD的语义,可为形式化分析软件体系结构层方面编织提供支持。     

基于系统理论过程分析的软件安全性需求分析与验证方法

针对传统系统理论过程分析（STPA）方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题，提出一种基于STPA的软件安全性需求分析与验证方法。首先，提取软件安全性需求，并利用算法将其转化为形式化表达式；其次，建立状态图模型来描述软件安全控制行为逻辑，并将其转化为程序可读的形式化语言；最后，采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性，结果表明，该方法能够实现安全需求分析的自动化生成与形式化验证，解决了传统方法对于人工干预的依赖问题及自然语言描述问题。     

基于SPEC#的自动测试方法

测试是软件质量的直接保障,然而人工书写测试代码不但繁琐而且会带来很多问题,自动化的测试方法的研究仍然停留在理论阶段.基于(SPEC# NUnit)平台,提出了一种切实可行的面向对象软件的自动化测试方法.这种方法使用形式化谓词断言来作为标准判断测试成功与否,搜索测试用例空间,同时可以模拟对象中间状态,自动生成复杂数据的测试用例.这一平台的建立也使得测试应绝对反映设计,由设计来直接指导测试的思想成为可能.     

Toward a Science of Power Management

This paper discusses how a formal understanding of energy and computation tradeoffs will open up new areas of investigation and lead to significantly more energy-efficient hardware and software designs while preserving the continued improvement in performance that the emerging applications demand. A formal approach will hopefully lead to energy-management solutions that are not only effective but also easy to implement and validate.     

Contributions to the semantics of logic perpetual processes

Summary Logic perpetual processes (logic programs with infinite data structures) have been given several formal (operational and fixpoint) semantics. In this paper, we compare the various semantics and define a formal characterization of a least fixpoint semantics, which is based on a modified version of the logic programs and which is satisfactory for a large class of logical perpetual processes. Our results show that all the proposed fixpoint semantics are not equivalent to the operational semantics and suggest an improvement of the least fixpoint approach.     

Achieving higher SEI levels

Two years or more can pass between formal SEI (Software Engineering Institute) assessments using the Capability Maturity Model (CMM). An organization seeking to monitor its progress to a higher SEI level needs a method for internally conducting incremental assessments. The author provides one that has proven successful at Motorola. A method was developed for assessing progress to higher SEI levels that lets engineers and managers evaluate an organization's current status relative to the CMM and identify weak areas for immediate attention and improvement. This method serves as an effective means to ensure continuous process improvement as well as grassroots participation and support in achieving higher maturity levels. This progress-assessment process is not intended as a replacement for any formal assessment instruments developed by the SEI, but rather as an internal tool to help organizations prepare for a formal SEI assessment. Although the author provides examples in terms of CMM version 1.1, both the self-evaluation instrument and the progress-assessment process are generic enough for use with any (similar) later version of the SEI CMM by updating the worksheets and charts used     

基于构件组装的项目管理系统开发研究

由于项目管理技术的不断提升和管理模式的多样化,不同行业甚至不同企业对项目管理系统的要求各不相同。如何利用软件构件技术快速地构造新的项目管理系统成为急需解决的问题。从项目管理系统的框架出发,首先对构件进行了形式化定义,然后基于此定义对项目管理系统组成部分进行了形式化描述,最后利用定义好的连接器,通过顺序、选择和并行三种组装方式组装成项目管理系统。并在此基础上提出了基于构件组装的PMS开发模型。     

Constraint-centric workflow change analytics

In a globalized economic environment with volatile business requirements, continuous process improvement needs to be done regularly in various organizations. However, maintaining the consistency of workflow models under frequent changes is a significant challenge in the management of corporate information services. Unfortunately, few formal approaches are found in the literature for managing workflow changes systematically. In this paper, we propose an analytical framework for workflow change management through formal modeling of workflow constraints, leading to an approach called Constraint-centric Workflow Change Analytics (CWCA). A core component of CWCA is the formal definition and analysis of workflow change anomalies. We operationalize CWCA by developing a change anomaly detection algorithm and validate it in the context of procurement management. A prototype system based on an open-source rule engine is presented to provide a proof-of-concept implementation of CWCA.     

结合形式化的面向对象设计方法与支撑系统

为了有效地结合形式化和非形式化设计方法各自的优点,克服其不足之处,以尽可能保证软件设计的质量与可靠性,文章提出了一种将形式化方法与非形式化的面向对象设计方法ＨＯＯＤ（ｈｉｅｒａｒｃｈｉｃａｌｏｂｊｅｃｔ－ｏｒｉｅｎｔｅｄｄｅｓｉｇｎ）相结合的途径,并介绍了其机器支撑环境的设计与实现．该途径在对层次式面向对象设计方法ＨＯＯＤ进行必要扩充的基础上,有机地集成了Ｚ语言等形式规约技术．支持这一途径的支撑环境提供了一套方便灵活的图形构筑工具、语法制导的形式语言与文本编辑工具,以及自动检查机制等．     

基于Pi演算的Web服务组合过程框架

文章从Web服务的编排、验证、部署角度提出了基于Pi演算的Web服务组合过程框架,说明了这个框架中每一步骤涉及的理论和工具应用。并在现有研究的基础上,针对框架中人工参与较多形式化验证环节提出了其向自动化、可视化方向发展的改进方法。