一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。     

一种适应动态不确定环境的规划系统POMDPRS的形式描述

规划是人工智能研究的一个重要方向,具有极其广泛的应用背景.POMDPRS是一种结合了PRS的持续规划机制、POMDP的概率分布信念模型和极大效用原理的持续规划系统.它具有较强的对动态不确定性环境的适应能力.本文试图在形式语义层面上对POMDPRS进行描述并举例将其与PRS和POMDP比较,进一步说明其优势.     

Formal Specification and Enactment of Security Policies through Agent Coordination Contexts

Our research moves from three fundamental considerations that concern the modelling and engineering of complex systems. First, organization, coordination and security are strictly related issues that should be modelled in a uniform and coherent framework. Second, models, technologies and methodologies should come hand in hand, so that abstractions used in the analysis and design stages should be still “alive and kicking” at development and execution time. Third, the general non-formalisability of complex systems should not prevent us from using formal tools whenever useful, such as in proving or ensuring properties of limited but meaningful portions of a system.By focussing on multi-agent systems, we discuss the notion of Agent Coordination Context (ACC) as an abstraction that (i) works as an organization and security abstraction, (ii) integrates well with abstractions provided by coordination infrastructures, and (iii) covers the engineering process from design to deployment. In particular, in this paper we study the syntax and semantics of a language for ACCs specification, exploiting typical process algebra techniques. Accordingly, we show that process algebras are a suitable tool for both specification and enactment of security and coordination policies through ACCs.     

面向方面分布式系统形式化规格说明语言

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。     

基于Object-Z的形式化验证方法

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合精确地描述大型软件系统,并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法,接着用Object-Z描述了一个电梯操作系统的实例,在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。     

状态图到PTL形式规范的转化

本文讨论从状态图到PTL形式规范的转化方法.状态图是描述系统行为的半形式化的图形工具,但缺少精确的形式语义,PTL(投影时序逻辑)是一种具有离散的时间模型的时序逻辑,把状态图转换到PTL后可以使其具有精确的形式语义并能使用形式化验证方法来证明状态图所描述的系统的一些重要性质是否得到满足,同时可把系统的形式描述转换为Tempura程序进行模拟,从而提高系统设计的可信性.     

面向对象的形式化规约语言GOOZ

在总结和评价现有Z语言面向对象扩充的基础上，设计了一种新的扩充语言GOOZ，该语言克服了Z＋＋，Object_Z等语言的一些缺点，其书写规约具有简洁，明确，接口定义清晰，模块无整，结构良好，易于验证的特点。     

Formal Specification and Verification of Distributed Systems

Computations of distributed systems are extremely difficult to specify and verify using traditional techniques because the systems are inherently concurrent, asynchronous, and nondeterministic. Furthermore, computing nodes in a distributed system may be highly independent of each other, and the entire system may lack an accurate global clock.     

Formal Techniques for Protocol Specification and Verification

Certain formal approaches, such as transition techniques and reachability analysis, show promising results when applied to protocol specification and verification.     

Formal Verification of Activity-Based Specification of Protocols

In this paper, we describe a method to formally verify activity-based specifications such as EBSDL. Starting from EBSDL-like specifications that specify engineering activities in terms of input and output behaviors, we derive programs in an asynchronous language CSP-R. CSP-R programs are then verified by the Maxpar method by composing them with the programs abstracting their environment. EBSDL-like specification and its verification using our method, is illustrated through the example of a fragment of LAPD protocol. The derivation of programs from the specification of activities of the underlying protocols through EBSDL-like specifications provides an important useful tool for formal verification of real-time protocols. We shall also discuss a translation of EBSDL-like specifications to synchronous languages such as Esterel. In the method proposed, it is possible for the user to choose asynchronous or synchronous formalisms depending upon the requirements of verification vis-a-vis logical specification.     

基于LOTOS形式规范的目标实现

LOTOS形式规范的目标实现是协议设计中必不可少的阶段之一。该文对基于LOTOS的形式描述规范的实现方法进行了研究,包括目标实现环境的特点、实现中的空白因素、抽象模型到实现模型的转换、规范的最终目标实现,并对如何将LOTOS规范转换为C、C 语言实现进行了探讨。     

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

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

形式化方法B及其程序规约机理

用形式化方法开发软件是提高软件可靠性和生产效率的革命性途径,是实现软件自动化的关键。文章针对B方法,介绍了其产生的历史背景,分析了其程序规约机理,并结合实例给出了B方法中抽象机的具体运用,对该方法的特点进行了评述。     

移动Agent系统的Z语言形式化描述

采用非形式化到形式化的过程：先用自然语言描述移动Agent，然后用形式语言Z及组件技术来描述移动Agent，并给出一个形式化的基础及移动Agent系统的一个精确高效的开发方法。     

An Approach to Formal Specification of Control Modules

This paper is concerned with the formal specification of program modules which control access to resources shared among concurrent proceses. The concept of state space is defined for such program modules and the formal specification is given in terms of a program module invariant and input-output assertions defined on the state space. Examples are provided to ilustrate the construction of sDecifications with this approach.     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

Applying Formal Specification to Software Development in Industry

This paper reports experience gained in applying formal specification techniques to an existing transaction processing system. The system is the IBM Customer Information Control System (CICS) and the work has concentrated on specifying a number of modules of the CICS application programmer's interface.