ZRC – A Refinement Calculus for Z

The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem. As an answer to that, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC. We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z. Received July 1997 / Accepted in revised form October 1998     

The lattice of data refinement

We define a general notion of data refinement that comprises the traditional notion of data refinement as a special case. Using the concepts of duals and adjoints, we define converse commands and find a symmetry between ordinary data refinement and a dual (backward) data refinement. We show how ordinary and backward data refinement are interpreted as simulation, and we derive rules for the piecewise data refinement of programs. Our results are valid for a general language, including demonic and angelic nondeterminism as well as nontermination and miracles.     

Model checking of state-rich formalism by linking to $$CSP\,\Vert \,B$$

International Journal on Software Tools for Technology Transfer - Since state-rich formalism is a combination of Z, CSP, refinement calculus and Dijkstra’s guarded commands, its model...     

Combining angels, demons and miracles in program specifications

The complete lattice of monotonic predicate transformers is interpreted as a command language with a weakest precondition semantics. This command lattice contains Dijkstra's guarded commands as well as miracles. It also permits unbounded nondeterminism and angelic nondeterminism. The language is divided into sublanguages using criteria of demonic and angelic nondeterminism, termination and absence of miracles. We investigate dualities between the sublanguages and how they can be generated from simple primitive commands. The notions of total correctness and refinement are generalized to the command lattice.     

Tightening the contract refinements of a system architecture

Contract-based design is an emerging paradigm for correct-by-construction hierarchical systems: components are associated with assumptions and guarantees expressed as formal properties; the architecture is analyzed by verifying that each contract of composite components is correctly refined by the contracts of its subcomponents. The approach is very efficient, because the overall correctness proof is decomposed into proofs local to each component. However, the process for the contract specification and refinement is quite expensive because the requirements are formalised into formal properties, where part of the complexity is delegated to the designer, who has the burden of specifying the contracts. Typical problems include understanding which contracts are necessary, and how they can be simplified without breaking the correctness of the refinement and other refinements in case some subcontracts are shared. In this paper, we tackle these problems by proposing a technique to understand and simplify the contract refinements of a system architecture during the development process for the contract specification and refinement. The technique, called tightening, is based on parameter synthesis. The idea is to generate a set of parametric proof obligations, where each parameter evaluation corresponds to a variant of the original(s) contract refinement(s), and to search for tighter variants of the contracts that still ensure the correctness of the refinement(s). We cast this approach in the OCRA framework, where contracts are expressed with LTL formulas, and we evaluate its performance and effectiveness on a number of benchmarks.     

Formalising and analysing the control software of the Compact Muon Solenoid Experiment at the Large Hadron Collider

The control software of the CERN Compact Muon Solenoid experiment contains over 27 500 finite state machines. These state machines are organised hierarchically: commands are sent down the hierarchy and state changes are sent upwards. The sheer size of the system makes it virtually impossible to fully understand the details of its behaviour at the macro level. This is fuelled by unclarities that already exist at the micro level. We have solved the latter problem by formally describing the finite state machines in the mCRL2 process algebra. The translation has been implemented using the ASF+SDF meta-environment, and its correctness was assessed by means of simulations and visualisations of individual finite state machines and through formal verification of subsystems of the control software. Based on the formalised semantics of the finite state machines, we have developed dedicated tooling for checking properties that can be verified on finite state machines in isolation.     

Exits in the refinement calculus

Although many programming languages contain exception handling mechanisms, their formal treatment — necessary for rigorous development — can be complex. Nevertheless, this paper presents a simple incorporation ofexit commands and exception blocks into a rigorous program development method. The refinement calculus, chosen for the exercise, is a method of developing imperative programs. It is based on weakest preconditions, although they are not used explicitly during program construction; they merely justify the general method. In the style of the refinement calculus, program development laws are given that introduce and allow the manipulation ofexits. The soundness of the new laws is shown using weakest preconditions (as for the existing refinement calculus laws). The extension of weakest preconditions needed to handleexits is a variation on earlier work of Cristian; the variation is necessary to handle nondeterminism.     

A Unified Pilot Training and Control System for Underwater Robotic Vehicles (URV)

This paper introduces the work done to improve on a sophisticated Underwater Robotic Vehicle (URV) inspection and repair system for submerged structures. It is undertaken as part of a research programme grant to pursue research and development of technologies and systems for the advancement of knowledge and for possible commercial exploitation relevant to the oil and gas industry. In particular, the paper focuses on the development of a unified pilot training and controls system that incorporates an advance man–machine interface for improving operator dexterity. Few formalised training procedures exist for URV pilots. In spite of the high cost, most URV pilots receive their training on-the-job. Training simulators can be viewed as a viable solution to this problem. Some attention has been made to address this problem. Notably are efforts by Imetrix URV-Mentor system, which focuses on VE simulation and on-line tutoring. Simulators, however, represents additional costs and in some ways lacks the realism of working on the real system. In the R ² C the researchers proposed a novel simulator configuration. We have developed a dual-purpose topside control system configuration that can be used for training as well as for on-line operation of an actual URV. In the simulator configuration, the physical URV is replaced by a simulator module, which accepts actual commands from the control system and responds with a simulated URV status, using a dynamic model of the URV. The simulator module behaves much like the actual URV accepting commands and responds with status information. The advantage of such a system is perceived to be lower system cost as well as a more realistic testing and simulation of the relevant processes.     

Sequential to parallel buffer refinement

This paper is intended to solve a particular problem related to the refinement of a shared sequential buffer into a parallel collection of buffers arising from a study on the IBM CICS project. Using the notion of cooperating refinement we show that the two systems are equivalent from the users' points of view (except with respect to efficiency). This is achieved by constructing an interleaving for each possible sequence of commands which access the buffer. The induction used in the proof is non-standard, and makes the problem harder than it would at first seem. Further we show that the interleaving cannot be done on the fly, showing that in some other sense, the parallel collection is indeed superior, as intuition suggests.This author was supported by the Esprit REX project     

Designing interactive interfaces: theoretical consideration of the complexity of standards and guidelines,and the difference between evolving and formalised systems

To design an interactive interface with communicative ability is a highly constrained, complex and difficult task. In the design process, a designer has to consider numerous principles, standards, and guidelines. It is impossible for a human being to consciously keep track of the interconnections between so many variables, or to calculate all the consequences that may emerge from putting all of the principles, standards, and guidelines together. This is often demonstrated in interaction with complex systems such as control rooms, surveillance systems, aeroplanes, especially when they display states (patterns) with which the user is not familiar. This is where the problems start. No artefact can display on its interface what has not been determined beforehand. If they could, it would mean that designers had the ability to predict all possible future states that the artefact may exhibit. As many complex artefacts function in a dynamic environment, it is simply impossible. There are two reasons why it is impossible to predict future states of a complex system, and hence to design communicative interfaces in an intelligible way. The first concerns the relationship between consciousness and the five omnipresent mental factors: contact, feeling, discernment, intention and attention. Secondly we note the essential difference between evolving and formalised communication systems: formalised systems are incapable of handling proliferating complexity, whereas proliferating complexity is a prerequisite for human development. Even though people appreciate natural complexity, which allows them to select and integrate information freely, they have difficulties in handling formalised complexity, which requires particular kinds of experience and logic. Hence, it is important to start a discussion about what kinds of formalised systems we should design. If we want to control systems, then they cannot be too complex, as we have difficulties coping with formalised complexity. If we want to create truly flexible systems, then we have to skip the control requirement.     

An application of Lyapunov stability analysis to improve the performance of NARMAX models

Previously we presented a novel approach to program a robot controller based on system identification and robot training techniques. The proposed method works in two stages: first, the programmer demonstrates the desired behaviour to the robot by driving it manually in the target environment. During this run, the sensory perception and the desired velocity commands of the robot are logged. Having thus obtained training data we model the relationship between sensory readings and the motor commands of the robot using ARMAX/NARMAX models and system identification techniques. These produce linear or non-linear polynomials which can be formally analysed, as well as used in place of “traditional robot” control code.In this paper we focus our attention on how the mathematical analysis of NARMAX models can be used to understand the robot’s control actions, to formulate hypotheses and to improve the robot’s behaviour. One main objective behind this approach is to avoid trial-and-error refinement of robot code. Instead, we seek to obtain a reliable design process, where program design decisions are based on the mathematical analysis of the model describing how the robot interacts with its environment to achieve the desired behaviour. We demonstrate this procedure through the analysis of a particular task in mobile robotics: door traversal.     

Posture control of robot manipulators with fuzzy voice commands using a fuzzy coach–player system

This paper presents a method of controlling robot manipulators with fuzzy voice commands. Recently, there has been some research on controlling robots using information-rich fuzzy voice commands such as 'go little slowly' and learning from such commands. However, the scope of all those works was limited to basic fuzzy voice motion commands. In this paper, we introduce a method of controlling the posture of a manipulator using complex fuzzy voice commands. A complex fuzzy voice command is composed of a set of fuzzy voice joint commands. Complex fuzzy voice commands can be used for complicated maneuvering of a manipulator, while fuzzy voice joint commands affect only a single joint. Once joint commands are learned, any complex command can be learned as a combination of some or all of them, so that, using the learned complex commands, a human user can control the manipulator in a complicated manner with natural language commands. Learning of complex commands is discussed in the framework of fuzzy coach–player model. The proposed idea is demonstrated with a PA-10 redundant manipulator.     

RCCSUS:一个实时控制命令情境理解模型系统

本文介绍一个实时控制命令情境理解模型ＲＣＣＳＵＳ（Ｒｅａｌ＿ｔｉｍｅＣｏｎｔｒｏｌＣｏｍｍａｎｄＳｉｔｕａｔｉｏｎａｌＵｎｄｅｒｓｔａｎｄｉｎｇＭｏｄｅｌＳｙｓｔｅｍ）的设计与实现。该系统模拟声控汽车实时命令的情境理解，对自然语言形式的控制命令结合动态变化的实时情境进行相应的真值理解，根据命令的正确与否作出相应的反应     

Statement inversion and strongest postcondition

A notion of inverse commands is defined for a language which permits both demonic and angelic nondeterminism, as well as miracles and nontermination. Every conjunctive and terminating command is invertible, the inverse being non-miraculous and disjunctive. A simulation relation between commands is described using inverse commands. A generalised form of inverse is defined for arbitrary conjunctive commands. The generalised inverses are shown to be closely related to strongest postconditions.     

A unification of probabilistic choice within a design-based model of reversible computation

We see reversible computing as a generalisation of sequential computation obtained by revoking the law of the excluded miracle. Our execution language includes naked guarded commands and non-deterministic choice. Choices which lead to miraculous continuations invoke reverse computation, and non-deterministic choice plays the rôle of provisional choice within a backtracking context. We require probabilistic choice for symmetry breaking and sampling large search spaces, but must formulate it differently from previous approaches to obtain the required interactions between probabilistic choice and non-deterministic choice and between probabilistic choice and feasibility. Our formulation allows us to derive the post-distributions which characterise a program, and we use these to construct a relational model. We consider refinement as containment of convex closures within distribution space, qualified with additional conditions to avoid over-refinement. We link the non-probabilistic and probabilistic versions of the model with a Galois connection and show that classical designs are a retract of our probabilistic designs. We consider the interaction between probabilistic and non-deterministic choice and find the same initially counter-intuitive results that have been noted by other investigators. We provide an alternative formulation, within the same model, of oblivious non-determinism, which allows all non-deterministic choices to be moved to the start of a computation. We consider the interaction between probabilistic choice and feasibility that is required to match an operational interpretation in which infeasible commands provoke reverse execution, and we present a small case study to show how the interaction between probabilistic choice and feasibility can be exploited in a practical program. All programming structures described here are supported by our implementation platform, the Reversible Virtual Machine, whose development has accompanied our theoretical investigations.     

FSCRIPT,a full portable text formatting program

FSCRIPT is a program designed to handle texts in an easy way. The text is given as card in an unformatted way together with the desired commands. These commands (there are 33 different commands) control the formatting of the text. FSCRIPT has been written in ANS FORTRAN.     

Controlling a robot manipulator with fuzzy voice commands using a probabilistic neural network

Natural language commands are generated by intelligent human beings. As a result, they contain a lot of information. Therefore, if it is possible to learn from such commands and reuse that knowledge, it will be a very efficient process. In this paper, learning from such information rich voice commands for controlling a robot is studied. First, new concepts of fuzzy coach-player system and sub-coach are proposed for controlling robots with natural language commands. Then, the characteristics of the subjective human decision making process are discussed and a Probabilistic Neural Network (PNN) based learning method is proposed to learn from such commands and to reuse the acquired knowledge. Finally, the proposed concept is demonstrated and confirmed with experiments conducted using a PA-10 redundant manipulator.     

A formal approach to the specification and transformation of constraints in MDE

This paper introduces a formal approach to constraint-aware model transformation which supports specifying constraints in the definition of transformation rules. These constraints are used to control which structure to create in the target model and which constraints to add to the created structure. The proposed approach is classified under heterogeneous, graph-based and out-place model transformations; and illustrated by applying it to a language translation. It is based on the Diagram Predicate Framework which provides a formalisation of (meta)modelling based on category theory and graph transformation. In particular, the proposed approach uses non-deleting transformation rules that are specified by a joined modelling language which is defined by relating the source and target languages. The relation between source and target languages is formalised by morphisms from their corresponding modelling formalisms into a joined modelling formalism. Furthermore, the application of transformation rules is formalised as a pushout construction and the final target model is obtained by a pullback construction.     

网络协同三维零件设计技术及系统研究

结合当前三维零件设计协同工作的需求，基于三维参数化特征设计、特征编码技术和网络通信技术，研究开发了具有C/S体系结构的三维零件设计工具。利用泛命令的思想，将造型命令卉分为网络命令和本地命令，大大减少了网络中传递的数据量；通过组织相应的网络数据结构，较好地实现了网络环境下零件级产品协同参数化造型设计。     

路由器配置诊断及优化系统研究与设计

路由器的配置错误在查找和定位上一直是诊断的难点,并且配置命令的无关联性也通常是造成配置出错的原因.路由器配置诊断系统能对配置命令分类找出其相关性,诊断并优化路由器配置.系统利用决策树算法生成配置命令的决策树,并从中提取有价值的配置命令的分类信息和规则,形成配置命令知识库.分析原有的配置文件,提取配置种类,利用知识库改进路由器的配置和诊断方法.系统简化了网络管理员的大部分的工作,将配置的错误率减到最低,并降低资源的消耗.