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     

一种离散事件系统实时控制器的设计

针对实时离散事件系统,提出了一种实时动态控制器的设计方法.用有限状态机FSM(Finite State Machine)对系统进行建模.用时态逻辑TL(Temporal Logic)给出系统的规范化要求.通过这两种形式化方法的有效结合,实现了控制器动态监控的功能.     

机床控制流程的一种有限状态机表达方法

面向过程的IEC-1131-3规范已难以满足机床 控制流程表达新的应用需求,为了更好地支持控制器开放式体系结构设计和面向对象系统实 现技术,我们扩展了有限状态机的基本概念,提出了一种机床控制流程表达的分层式有限状 态机(FSM)方法．本文首先对分层式FSM的组织方法、特性、形式定义等进行了详细讨论;为 了进一步阐明这种方法的表达特性,我们介绍了一种分层式FSM表达的机床控制器总体结构 ,并讨论了这种结构下的开放性设计表达和系统实现等相关问题．     

A New Formal Method for Communication Protocol Specification

A new formal method for communication protocol specification is presented.FSM,CSP and ADT are mixed and the best features of these approaches can be offered in the fomal method.First,we briefly describe the formal techniques of communication protocol.We then put forward the hybrid method of protocol specification.Finally,an example,i.e.,IEEE 802.3 MAC protocol for LAN described by the proposed formal method,is given.The results of studies show that this hybrid formal method for protocol specification is a correct,unambiguous and complete approach.     

The design and analysis of real-time systems using the ASTRAL software development environment

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the ASTRAL Software Development Environment (SDE), which is an integrated set of design and analysis tools based on the ASTRAL formal framework. The tools that make up the support environment are a syntax-directed editor, a specification processor, a verification condition generator, a browser kit, a model checker, and a mechanical theorem prover. This revised version was published online in June 2006 with corrections to the Cover Date.     

Global transaction support for workflow management systems: from formal specification to practical implementation

In this paper, we present an approach to global transaction management in workflow environments. The transaction mechanism is based on the well-known notion of compensation, but extended to deal with both arbitrary process structures to allow cycles in processes and safepoints to allow partial compensation of processes. We present a formal specification of the transaction model and transaction management algorithms in set and graph theory, providing clear, unambiguous transaction semantics. The specification is straightforwardly mapped to a modular architecture, the implementation of which is first applied in a testing environment, then in the prototype of a commercial workflow management system. The modular nature of the resulting system allows easy distribution using middleware technology. The path from abstract semantics specification to concrete, real-world implementation of a workflow transaction mechanism is thus covered in a complete and coherent fashion. As such, this paper provides a complete framework for the application of well-founded transactional workflows. Received: 16 November 1999 / Accepted 29 August 2001 Published online: 6 November 2001     

A Formal and Tool-Equipped Approach for the Integration of State Diagrams and Formal Datatypes

Separation of concerns or aspects is a way to deal with the increasing complexity of systems. The separate design of models for different aspects also promotes a better reusability level. However, an important issue is then to define means to integrate them into a global model. We present a formal and tool-equipped approach for the integration of dynamic models (behaviors expressed using state diagrams) and static models (formal data types) with the benefit to share advantages of both: graphical user-friendly models for behaviors, formal and abstract models for data types. Integration is achieved in a generic way so that it can deal with both different static specification languages (algebraic specifications, Z, B) and different dynamic specification semantics     

Formal interaction specification in public health surveillance systems using pi-calculus

This paper provides formal specification of interactions in typical public health surveillance systems involving healthcare agencies at local, state and federal levels. Although few standards exist for exchange of healthcare information, there is a general lack of formal models of the protocols involved in the interactions between the agencies. The quality of medical care provided is an end result of a well designed choreography of diverse services provided by different healthcare entities. One of the major challenges in this field appears to be explicit formal specification of such interactions. Such formal specification work is the first step leading to both design and verification of important properties of public healthcare systems. pi-calculus is a formal modeling technique for precise specification of semantics in interacting concurrent systems where mobility is involved. Two different configurations of public health surveillance systems are modelled using pi-calculus in this paper.     

Transformation of a language L* specification of an FSM into an automata equivalent specification in the language L

A method is proposed to transform an FSM specification in the language L* into a specification in the language L. Using additional predicate symbols, the former specification is first transformed into a specification of an FSM with finite memory. Then this specification is transformed into an automata equivalent specification in the language L.     

多单元协议一致性测试中的同步序列的生成

有限状态机模型一般被用来描述通信协议和其它各类的分布式系统,对于一个多端口的有限状态机,需要多个测试单元进行测试,使用一个包括K个（K≥2）测试单元的测试系统可以检查一个多单元通信协议软件的收发行为是否与协议规格一致,在测试过程中,K个测试单元之间可能会出珊步问题,目前,主要是通过增加外部同步操作来解决同步问题,提出了一种新的同步测试序列生成模型－－同步有向图,它可以判断一个给定的协议规格是否可以在不需要外部同步操作的情况下,产生同步测试序列;如果可以产生,则此生成中以将非同步测试相应的同步测试序列;另外此生成模型还可以用来选择为测试系统增加外部同步通道的方法。     

The Meta-Protocol framework

A communication protocol is a set of rules shared by two or more communicating parties on the sequence of operations and the format of messages to be exchanged. Standardization organizations define protocols in the form of recommendations (e.g., RFC) written in technical English, which requires a manual translation of the specification into the protocol implementation. This human translation is error-prone due in part to the ambiguities of natural language and in part due to the complexity of some protocols. To mitigate these problems, we divided the expression of a protocol specification into two parts. First, we designed an XML-based protocol specification language (XPSL) that allows for the high-level specification of a protocol—expressed as a Finite State Machine (FSM)—using Component-Based Software Engineering (CBSE) principles. Then, the components required by the protocol are specified in any suitable technical language (formal or informal). In addition, we developed the multi-layer Meta-Protocol framework, which allows for on-the-fly protocol discovery and negotiation, distribution of protocol specifications and components, and automatic protocol implementation in any programming language.     

Modeling of a dynamic dual-input dual-output fast steeringmirror system

A modeling method is proposed for a dynamic fast steering mirror (FSM) system with dual inputs and dual outputs. A physical model of the FSM system is derived based on first principles, describing the dynamics and coupling between the inputs and outputs of the FSM system. The physical model is then represented in a state-space form. Unknown parameters in the state-space model are identified by the subspace identification algorithm, based on the measured input-output data of the FSM system. The accuracy of the state-space model is evaluated by comparing the model estimates with measurements. The variance-accounted-for value of the state-space model is better than 97%, not only for the modeling data but also for the validation data set, indicating high accuracy of the model. Comparison is also made between the proposed dynamic model and the conventional static model, where improvement in model accuracy is clearly observed. The model identified by the proposed method can be used for optimal controller design for closed-loop FSM systems. The modeling method is also applicable to FSM systems with similar structures.     

移动组件系统模型的分析与描述

移动计算是新兴的分布式计算范型,其主要特征是计算组件与计算场所能动态改变绑定关系,表现出移动性,从而带来许多新的系统设计需求.从系统模型层次角度对位置、移动组件、移动和资源访问等移动计算核心概念,以及组件与位置之间的各种关系和关系变化刻画的移动范型进行了描述.通过使用集合论和操作语义的规约规则形式地表示这些概念、关系和移动机制,进而抽象出移动系统设计所需的语言结构,为移动系统设计和开发提供了分析基础.     

The Input Model of Standard Graphics Systems Revisited by Formal Specification

This paper describes the specification of an input model for graphics systems. The initial aim of the work reported in this paper was to revise the input model adopted by graphics standards by means of formal specification techniques in order to acquire a deep knowledge of its capabilities, to eventually discover errors and to develop improvements. Taking into account similar works done in this area by others and considering a number of major issues related to input recently discussed within the graphics community, a new model is being proposed that addresses the very key concepts of parallelism, extensibility and reconfigurability. The model is based upon composition operations defined over basic components specified as a set of concurrent processes. Composition operations and process definitions have been formally specified by using the LOTOS notation and investigated by means of the LOTOS Interactive Tools Environment. In the first part of the paper, the input model of graphics standards is shortly examined in the light of the results so far achieved by related works on formal specification of computer graphics systems. Subsequently, an improved model is presented. Finally, its capability of simulating the traditional operating modes of logical input devices and a methodology for defining new operating modes is demonstrated.     

数据库系统应用基准测试规范设计方法

为准确度量数据库系统对领域应用系统的支撑能力,提出了一种应用基准测试规范设计方法,指导数据库系统的基准测试。提出以动作、环境、负载等信息项为框架,建立数据库系统使用需求集,规范初始信息格式;将使用需求初分为操作场景,建立关键变量矩阵,并应用K-means算法、层次式聚类等方法进行操作场景分组,确认典型应用系统集;设计了基准测试用例结构,提出了环境要求、事务要求、执行要求等重要信息项,并构建测试规范框架,描述了典型应用系统与应用基准测试规范的关系;通过实例应用,证明了该方法的可行性与适用性。所提方法可辅助解决应用系统在多个数据库系统中择优选型问题,也可用于数据库系统厂商自测,促进产品能力提升。     

Fictitiousness analysis of states of a finite-state machine synthesized from its specification transformed from the language L* to the language L

A method for synthesizing an FSM from its specification in the logical language L* is considered. The method is based on translating such a specification into the less expressive language L and applying an available method for synthesizing the sought-for FSM from the specification in this language. The resulting FSM may contain redundant states that are called fictitious and must be eliminated. A simple method for checking states for fictitiousness is proposed.