Better Understanding through Formal Specification

The Graphical Kernel System (GKS) is now registered as an ISO International Standard for computer graphics programming. One of the major innovations of the Standard is the bundled specification of aspects, a mechanism which gives the applications programmer the ability to tailor the appearance of a picture independently on each of the workstations on which it is displayed, using the capabilities of the workstations. GKS also incorporates the traditional method of individual specification of aspects in which each workstation does the best it can to represent global aspect values. In this paper a formal specification technique, the Vienna Development Method (VDM), is used to describe aspect specification. The GKS model of aspect specification is progressively constructed from simpler models. Properties of these simpler models are formulated and the specifications are proved to conform to these. The properties are then traced through the more complex models. The paper demonstrates the applicability of formal specification to the design of graphics software and the ability of formal techniques to catalyse the deeper understanding of designs.     

Formal Specification in the Revision of GKS: An Illustrative Example

The first ISO/IEC standard for computer graphics, the Graphical Kernel System (GKS) was published in August 1985. In accordance with ISO/IEC procedures, GKS is now being reviewed and revised. This paper describes how formal specification techniques are being used by the authors to analyse key parts of proposals being made for changes to the framework of GKS to bring the standard into line with the requirements of applications and the operating environment likely to be found in the mid-1990's.     

The GKS Input Model in Manifold

This paper describes the specification of the GKS input model in M anifold . The aim of the work reported in this paper was two-fold: first, to review the communication patterns implied by the GKS input model, and second, to evaluate the suitability of the M anifold language as a tool for defining complex dynamic interaction patterns that are common in non-trivial user interfaces.
The GKS input model is also adopted by all more recent ISO graphics standard documents. A more formal scrutiny of the inter-communication of the components of this model, excluding the implementation details of their functionality, is instructive in itself. It can reveal directions for improvement of its shortcomings and for generalization of its strengths for the ongoing effort to define the functionality of future graphics packages.
M anifold is a language for describing inter-process communications. Processes in M anifold communicate by means of buffered communication links called streams and by reacting to events raised asynchronously by other processes. Our experience shows that M anifold is a promising tool for describing systems of cooperating parallel processes. Our M anifold specification of the GKS input model offers a very flexible way to structure user defined logical input devices. Furthermore, it is simple and modular enough to allow easy extensions to include more functionality by local modifications. As such, it can serve as a basis for possible extensions and enhancements envisioned for future graphics packages.
1987 CR Categories: C.1.2, C.1.3, C.2.m, D.1.3, F.1.2, I.1.3, I.3.6, I.3.4.
1885 Mathematical Subject Classification: 68N99, 68Q10,68U05.     

Functional conformance testing of graphics software using a configurable reference system

This paper introduces a scheme for conformance checking of GKS implementations with the given GKS standard specification[1] based on functional black box testing. Specific testing problems caused by the nature of graphics systems and a solution are presented. Thereby emphasis is laid on a software generation technique which allows to configure reference implementations from a suitable specification of GKS. The reference implementation is used to produce correct reference data the contents and formats of which are adjusted for the particular candidate implementation.     

一个Object-Z规格说明的证明责任产生器

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。     

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

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

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

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

HB协议的形式规约与验证

形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.     

网络协议设计中形式结构模型的创建方法研究

形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法。简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格。基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性。     

Towards a formal definition of methods

The absence of a formal specification of methods permits application engineers to interpret method concepts in any way they want. Further, different CASE tool designers can implement the same method concepts in different ways. The approach to formal method specification described here is in three levels: the generic level, the method independent level, and the method level. The generic level provides a model of a method which can be instantiated to yield a method-independent view of methods. This view can, in turn, be instantiated to yield the formal method of interest. The attempt is to represent methods independently of any underlying way-of-working or paradigm, remove the process/product dichtomy by tight coupling of the process and product aspects of methods, and permit extensibility of methods. The formal specification can be used as a basis for building CASE tools, as an output to be produced by a CAME tool, and for defining development processes.     

基于UML规格说明测试用例生成工具

利用UML状态图,采用基于状态的测试数据生成标准生成测试用例。其中UML状态图是测试用例生成的关键部分,在某种意义上,UML状态图能够图容易生成测试用例。     

Using a formal specification contractually

A commonly made criticism of formal methods is that they increase costs. Selective use of formal methods to define critical requirements can, however, lead to a significant decrease in lifecycle costs. In particular the economic and technical benefits of outsourcing the development of software can be fully realized and the cost of outsourcing slightly reduced by use of a formal specification. In this paper we describe a development in which a formal specification prepared by the customer formed part of the contract with the supplier. We conclude that this use of a formal specification can reduce risks and costs for all concerned and can help foster fruitful and co-operative relations in situations which are often fraught with confrontation.Published with the permission of the controller of Her Britannic Majesty's Stationery Office.     

MAP载波带局域网MMS程序调用服务的形式化描述

网络协议的形式化描述对于协议的定义，协议的正确性验证以及协议的实施有着非常重要的意义，本文采用有限状态自动机的方法对制造自动化协议的关键部分ＭＭＳ的程序调用服务进行了形式化的描述。     

Software specification using the special language

This paper presents a tutorial overview of special, a formal specification and assertion language created by SRI International as part of their hierarchical design methodology. The language is based on a formal model of system behavior and is supported by language processors that assist in the interactive development of specifications. special is a strongly typed language that models data and programs as abstract resources known as objects. Collections of modules known as abstract machines are the major building blocks of a software specification in special. The technical foundations of special and the components of a special specification are described. A sample specification is detailed in an appendix.