Towards action refinement for true concurrent real time

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper we develop a theory of action refinement in a real-time non-interleaving causality based setting, a timed extension of bundle event structures that allows for urgent interactions to model timeout. The syntactic action refinement operation is presented in a timed process algebra as incorporated in the internationally standardised specification language LOTOS. We show that the behaviour of the refined system can be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions with explicitly represented start points, that the timed versions of a linear-time equivalence, termed pomset trace equivalence, and a branching-time equivalence, termed history preserving bisimulation equivalence, are both congruences under the refinement, and that the syntactic and semantic action refinements developed coincide under these equivalence relations with respect to a metric denotational semantics. Therefore, our refinement operations behave well. They meet the commonly expected properties.Received: 9 January 2003     

A Highly Scalable GALS Crossbar Using Token Ring Arbitration

With increases in die size and clock frequency, driving signals across dies is becoming increasingly more difficult. To reduce clock skew and power, the general trend is to use multiple clock domains on a single die, making both synchronous and asynchronous interclock domain communication possible. The 2005 International Technology Roadmap for Semiconductors states that asynchronous global signaling is required to handle multiple clock domains. According to the ITRS, the globally asynchronous, locally synchronous (GALS) methodology should address this problem. This methodology enables the use of a clocked design for smaller-scale functional units, and this has been the standard approach in industry. The GALS methodology also makes it possible to connect synchronous functional units using robust asynchronous interconnects. The efficient design of an asynchronous crossbar is one of the most promising implementations of the GALS methodology. In this article, we present a low-latency crossbar that uses a distributed arbitration mechanism in the form of token rings. We further improve the latency of this implementation by implementing asynchronous-to-synchronous and synchronous-to-asynchronous interface logic using bidirectional signals. These signals serve as requests and acknowledges, and they exhibit a very fast GasP-like implementation - although, unlike GasP, this implementation is not self-resetting.     

双三轴仿真转台同步控制系统研究

双三轴仿真转台的同步控制和动态特性指标关系到导航与制导系统的优劣。针对双转台之间的时钟同步问题,提出基于IEEE1588时钟同步协议和光纤反射内存网的时钟同步方法,通过时间服务器接收GPS或北斗时钟时间信号输出1 ms方波,进一步通过光纤反射内存网络进行时钟脉冲分发实现不同系统之间的时钟同步。针对原本双转台动态同步控制需要手动精调同步参数且容易出现超调现象的不足,提出一种基于参考模型自适应的同步控制方法,以其中一台性能较好的转台作为参考模型,另一台性能较差的转台通过自适应算法进行跟踪控制,从而实现双转台之间的同步控制。通过仿真验证和实验验证,证明该算法稳定可靠,易于实现,可以有效地提高双转台之间的动态同步特性。     

命令式动态规划类算法程序推导及机械化验证

动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.     

Existence and Verification for Decentralized Nondeterministic Discrete‐Event Systems Under Bisimulation Equivalence

In this paper, we study the decentralized control problem for nondeterministic discrete‐event systems (DESs) under bisimulation equivalence. In order to exactly achieve the desired specification in the sense of bisimulation equivalence, we present a synchronous composition for the supervised system based on the simulation relation between the specification and the plant. After introducing the notions of simulation‐based controllability and simulation‐based coobservability, we present the necessary and sufficient condition for the existence of a decentralized supervisor such that the controlled system is bisimilar to the specification, and an algorithm for verifying the simulation‐based coobservability is proposed by constructing a computational tree.     

Action Refinement for Real-Time Concurrent Processes with Urgency

Action refinement for real=time concurrent processes with urgent interactions is studied, where a partial-order setting, i.e., timed bundle event structures, is used as the system model and a real-time LOTOS-like process algebra is used as the specification language. It is shown that the proposed refinement approaches have the commonly expected properties:(1) the behaviour of the refined process can be inferred compositionally from the behaviour of the original process and from the behaviour of the processes substituted for actions; (2) the timed extensions of pomset (partially ordered multiset) trace equivalence and history preserving bisimulation equivalence are both congruences under the refinement; (3) the syntactic and semantic refinements coincide up to the aforementioned equivalence relations with respect to a cpo-based denotational semantics.     

Verification of Mondex electronic purses with KIV: from transactions to a security protocol

The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation. J. C. P. Woodcock     

Composition and Refinement of Specifications of Parameterized Data Types

In [5] we introduced a framework for specification of parameterized data types utilizing a generalization of the traditional semantics based on the pushout construction. In the present paper, we address the issue of program development using this framework with particular emphasis on the notion of refinement. Unlike for the loose specifications, refinement does not amount merely to a narrowing of the model class, but primarily to introduction of additional structure into the specified program. We give examples based on the analogues of the classical vertical and horizontal composition of such specifications.     

基于过程级编程模型的软硬件协同设计框架

当前动态可重构计算系统对程序员编程不透明,且动态可重构资源难以有效利用。针对上述问题,提出一种基于过程级透明编程模型的软硬件协同设计框架。在该框架内,软件开发人员对软硬件协同函数库进行调用,即可用C语言完成系统功能描述。动态软硬件划分算法在程序运行时进行划分,自动选择并调度需要转换到软件或硬件的库函数,通过动态链接器实时切换函数的运行方式,实现由功能描述到系统实现的自动化流程。     

Laws of data refinement

Summary A specification language typically contains sophisticated data types that are expensive or even impossible to implement. Their replacement with simpler or more efficiently implementable types during the programming process is called data refinement. We give a new formal definiton of data refinement and use it to derive some basic laws. The derived laws are constructive in that used in conjunction with the known laws of procedural refinement they allow us to calculate a new specification from a given one in which variables are to be replaced by other variables of a different type.     

A sequential real-time refinement calculus

We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time specifications. A specification may include not only execution time limits, but also requirements on the behaviour of outputs over the duration of the execution of the program. The approach allows refinement steps that separate timing constraints and functional requirements. New rules are provided for handling timing constraints, but the refinement of components implementing functional requirements is essentially the same as in the standard refinement calculus. The product of the refinement process is a program in the target programming language extended with timing deadline directives. The extended language is a machine-independent, real-time programming language. To provide valid machine code for a particular model of machine, the machine code produced by a compiler must be analysed to guarantee that it meets the specified timing deadlines. Received: 27 September 1997 / 13 June 2000     

Behavioural specification for hierarchical object composition

Behavioural specification based on hidden (sorted) algebra constitutes one of the most promising recently developed formal specification and verification paradigms for system development.Here we formally introduce novel concepts of behavioural object and equivalence between behavioural objects within the hidden algebra framework. We formally define several object composition operators on behavioural objects corresponding to the hierarchical object composition methodology introduced by CafeOBJ. We study their basic semantical properties and show that our most general form of behavioural object composition with synchronisation has final semantics and a composability property of behavioural equivalence supporting a high reusability of verifications. We also show the commutativity and the associativity of parallel compositions without synchronisation.     

A Survey and Taxonomy of GALS Design Styles

Single-clocked digital systems are largely a thing of the past. Although most digital circuits remain synchronous, many designs feature multiple clock domains, often running at different frequencies. Using an asynchronous interconnect decouples the timing issues for the separate blocks. Systems employing such schemes are called globally asynchronous, locally synchronous (GALS). To minimize time to market, large SoC designs must integrate many functional blocks with minimal design effort. These blocks are usually designed using standard synchronous methods and often have different clocking requirements. A GALS approach can facilitate fast block reuse by providing wrapper circuits to handle interblock communication across clock domain boundaries. SoCs may also achieve power savings by clocking different blocks at their minimum speeds. For example, Scott et al. describe the advantages of GALS design for an embedded-processor peripheral bus.     

Weighted modal transition systems

Specification theories as a tool in model-driven development processes of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature, and therefore fragile in the sense that the inevitable approximation of systems by models, combined with the fundamental unpredictability of hardware platforms, makes it difficult to transfer conclusions about the behavior, based on models, to the actual system. Hence this approach is arguably unsuited for modern software systems. We propose here the first specification theory which allows to capture quantitative aspects during the refinement and implementation process, thus leveraging the problems of the qualitative setting. Our proposed quantitative specification framework uses weighted modal transition systems as a formal model of specifications. These are labeled transition systems with the additional feature that they can model optional behavior which may or may not be implemented by the system. Satisfaction and refinement is lifted from the well-known qualitative to our quantitative setting, by introducing a notion of distances between weighted modal transition systems. We show that quantitative versions of parallel composition as well as quotient (the dual to parallel composition) inherit the properties from the Boolean setting.     

一种基于定制高性能互连的对象存储系统

基于高性能互连实现对象存储系统已经成为构建高性能计算机可扩展I/O系统的发展趋势。我们设计并实现了一种定制的高带宽、低延迟的高性能互连芯片HSNI,它提供了很好的通信性能,可用于构建对象存储系统。本文对HSNI的硬件体系结构、软件结构及其通信机制进行了介绍,并基于HSNI构建了高性能的对象存储系统。性能测试结果表明,HSNI芯片带宽高、延迟低,非常适合构建大规模对象存储系统,该存储系统能够很好地发挥Lustre系统的性能,并具有很好的可扩展性,能够很好地满足面向高性能计算的I/O系统需求。     

TOWARDS PARALLEL PROGRAMMING BY TRANSFORMATION: THE FAN SKELETON FRAMEWORK*

A Functional Abstract Notation (FAN) is proposed for the specification and design of parallel algorithms by means of skeletons - high-level patterns with parallel semantics. The main weakness of the current programming systems based on skeletons ii that the user is still responsible for finding the most appropriate skeleton composition for a given application and a given parallel architecture

We describe a transformational framework for the development of skeletal programs which is aimed at filling this gap. The framework makes use of transformation rules which are semantic equivalences among skeleton compositions. For a given problem, an initial, possibly inefficient skeleton specification is refined by applying a sequence of transformations. Transformations are guided by a set of performance prediction models which forecast the behavior of each skeleton and the performance benefits of different rules. The design process is supported by a graphical tool which locates applicable transformations and provides performance estimates, thereby helping the programmer in navigating through the program refinement space. We give an overview of the FAN framework and exemplify its use with performance-directed program derivations for simple case studies. Our experience can be viewed as a first feasibility study of methods and tools for transformational, performance-directed parallel programming using skeletons.     

Dynamic frequency and voltage scaling for a multiple-clock-domain microprocessor

Multiple clock domains is one solution to the increasing problem of propagating the clock signal across increasingly larger and faster chips. The ability to independently scale frequency and voltage in each domain creates a powerful means of reducing power dissipation. A multiple clock domain (MCD) microarchitecture, which uses a globally asynchronous, locally synchronous (GALS) clocking style, permits future aggressive frequency increases, maintains a synchronous design methodology, and exploits the trend of making functional blocks more autonomous. In MCD, each processor domain is internally synchronous, but domains operate asynchronously with respect to one another. Designers still apply existing synchronous design techniques to each domain, but global clock skew is no longer a constraint. Moreover, domains can have independent voltage and frequency control, enabling dynamic voltage scaling at the domain level.     

A synchronous π-calculus

The SL synchronous programming model is a relaxation of the Esterel synchronous model where the reaction to the absence of a signal within an instant can only happen at the next instant. In previous work, we have revisited the SL synchronous programming model. In particular, we have discussed an alternative design of the model, introduced a CPS translation to a tail recursive form, and proposed a notion of bisimulation equivalence. In the present work, we extend the tail recursive model with first-order data types obtaining a non-deterministic synchronous model whose complexity is comparable to the one of the π-calculus. We show that our approach to bisimulation equivalence can cope with this extension and in particular that labelled bisimulation can be characterised as a contextual bisimulation.