规格说明语言NUSL及其支撑系统

本文简述了形式规格说明技术的意义,与原型技术的关系,并叙述了规格说明语言NUSL的特点、结构和使用,然后介绍了NUSL支撑系统.     

一种基于JSD方法的规格说明语言及其支撑系统的设计与开发

Jackson系统开发方法(JSD)是八十年代初提出的一种很有名的操作式软件开发方法。为了支持开发者将其应用到软件开发实践中,我们设计了一种基于JSD方法的图形化的操作式规格说明语言NUJSDL,并开发了其支撑系统NUJSDS,NUJSDL语言具有易理解、可分析和可维护等特性,它提供了多种机制分别刻划JSD开发过程中各阶段的结果,并且用它书写的规格说明还可以作为待开发系统的一个原型。NUJSDS是编辑工具分析工具规格说明生成工具和转换工具集成起来的交互式可扩充的系统,它支持规格说明在JSD思想指导下的开发     

网络通信协议的属性文法规格说明

本文给出一个基于属性文法的网络通信协议的形式说明与自动生成的模型.首先引入了一个扩展的属性文法描述工具,讨论了用其描述协议的并行、同步、延时（时序）等特性的有关问题；然后研究了基于属性文法的网络通信协议自动生成环境及其核心算法——属性计算（即语义分析）算法.     

关于Z规格说明语言中模式的剖析

1.引言形式规格说明语言一般是提供一套称为语法域的记号系统和一个称为语义域的对象集合,以及一组精确地定义哪些对象满足哪个规格说明的规则。规格说明是语法域中的句子。它用数学表示法精确地描述了软件系统必须具备的性质。 Z是目前比较流行的一种形式规格说明语言,它以一阶谓词逻     

规格说明语言Z的类型检查

软件规格说明的正确性是软件目标代码正确性的前提。正确性要求这一就是类型正确。本文介绍Ｚ规格说明类型的检查器的实现方法,并对类型检查的环境、一致化方法、替换策略和类型变量的应用等问题进行讨论。     

Z规格说明构造方法

比较完整地描述了Ｚ规格说明的结构和写规格说明的的步骤,并通过一个所设计的Ｚ规格说明的实例演示用Ｚ规格说明的过程。     

一个面向JSD方法的规格说明语言转换系统

ＪＳＬＣ系统是一个规格说明语言ＪＳＬ的转换系统．它的实现反映了一种规格说明语言的转换方法．本文详细介绍了ＪＳＬＣ系统的组成结构、实现基础和技术要点．     

协议形式化开发环境的规范语言

LOTOS（languageoftemporalorderingspecification）是一种基于进程代数CCS的协议规范语言，面向协议验证，但它不能描述协议的某些性质．本文提出了一种LOTOS的扩充语言ELOTOS（extendedLOTOS），它在LOTOS的基础上引入了异步通讯机制、时间描述、事件发生的随机性描述．     

可重用构件及其描述语言

本文讨论可重用构件应该具备的特性，并介绍一种可重用构件描述语言Ｒｅｃｏｓ．Ｒｅｃｏｓ支持面向对象设计，而且提供功能抽象和类属机制．     

一种适用于过程控制系统建模的形式描述语言PROTOB

本文研讨一种适用于过程控制系统建模的描述语言ＰＲＯＴＯＢ。文中首先阐述了ＰＲＯＴ网的基本概念及其实例，在此基础上讨论了ＰＲＯＴＯＢ网，结合一个过程控制系统的控制流程，给出了它的ＰＲＯＴＯＢ模型 。     

局部网络运输协议的形式描述与验证

本文研讨局部网络的运输协议及其形式描述技术.文中论述了局部网络建立运输层的必要性和可能性.讨论了局部网络体系结构中的运输层、运输服务和运输协议的设计,给出了该运输协议的一种基于有限状态自动机(FSA)的形式描述,并通过可达树对该协议的正确性进行了验证.     

DFA模型及其语言的结构化代数规约

本文首先阐述了利用ＤＦＡ模型技术进行状态转换系统描述存在的主要问题,提出了利用代数规约技术解决这些问题的可行性,然后介绍了新一代具有松散语义的代数规约语言ＳＰＥＣＴＲＵＭ及其主要规约操作符的语法和语义,并根据ＤＦＡ模型及其语言的数学定义,给出了它们的结构化代数规约,为基于ＤＦＡ模型的状态转换系统的形式化设计和开发奠定了基础。     

用Z语言形式化扩展事件踪迹图

软件体系结构被看成是现代软件技术的重要因素之一 ,而一个软件系统结构的关键就是它可以分解成组件和组件交互的规格说明。扩展事件踪迹图 (ExtendedEventsTraces ,EETs)是一种用来描述组件交互的图形技术 ,它允许我们用图来定义结构中经常发生的交互模型 ,并且在多种上下文中可实例化 ,因而可以重用。虽然EETs的图形表示很直观 ,但是语义不够精确 ,因此 ,在本文中将使用形式规格说明语言Z来形式化EETs。并且 ,给出了形式描述EETs的几个应用例子     

一个基于属性文法的通信协议形式描述语言及协议开发环境

通信协议是网络技术的核心。由于异质构环境中网络协议固有的复杂性,因此需要研制一磁建立在严格数学模型基础这之上的协议开发方法和集成工具环境,以降低协议开发难度,提高协议开发效率。本文旨在探索一种用于协议形式描述和工程开发的扩展属性文法,重点研究了设计属性文法描述语言的原理及结构特点等,并通过一个完整例子说明如何使用我们所设计的属性文法描述语言Ｌ＿ＰＳＡＧ定义一个协议,然后给出一个基于属性文法的协议设     

DECLARATIVE SPECIFICATION OF FAULT TOLERANT AUCTION PROTOCOLS: THE ENGLISH AUCTION CASE STUDY

Auction mechanisms are nowadays widely used in electronic commerce Web sites for buying and selling items among different users. The increasing importance of auction protocols in the negotiation phase is not limited to online marketplaces. In fact, the wide applicability of auctions as resource‐allocation and negotiation mechanisms have also led to a great deal of interest in auctions within the agent community. A challenging issue for agents operating in open Multiagent Systems (such as the emerging semantic Web infrastructure) concerns the specification of declarative communication rules which could be published and shared allowing agents to dynamically engage well‐known and trusted negotiation protocols. To cope with real‐world applications, these rules should also specify fault tolerant patterns of interaction, enabling negotiating agents to interact with each other tolerating failures, for instance terminating an auction process even if some bidding agents dynamically crash. In this paper, we propose an approach to specify fault tolerant auction protocols in open and dynamic environments by means of communication rules dealing with crash failures of agents. We illustrate these concepts considering a case study about the specification of an English Auction protocol which tolerate crashes of bidding agents and we discuss its properties.