Compatibility of parameter passing and implementation of parameterized data types

The basis for this paper are the concepts of parameterization and implementation of abstract data types which have been developed in the theory of algebraic specifications with initial algebra semantics. In this paper we combine both concepts defining implementations of parameterized data types and studying the compatibility of parameter passing and implementation of parameterized data types. In our main result we show that parameter passing commutes with implementation. This is an important step in order to apply the theory of algebraic specifications to development and stepwise refinement of software systems. We illustrate our notion and results by a small example implementing binary trees over arbitrary data by corresponding strings with brackets. Finally we consider the problem of 2-dimensional compatibility of parameter passing and implementation and discuss the kind of compatibility results which have been shown by other authors in the case of loose and final algebra semantics.     

Modular correctness proofs of behavioural implementations

We introduce a concept of behavioural implementation for algebraic specifications which is based on an indistinguishability relation (called behavioural equality). The central objective of this work is the investigation of proof rules which allow us to establish the correctness of behavioural implementations in a modular (and stepwise) way and, moreover, are practicable enough to induce proof obligations that can be discharged with existing theorem provers. Under certain conditions our proof technique can also be applied for proving the correctness of implementations based on an abstraction equivalence between algebras in the sense of Sannella and Tarlecki. The whole approach is presented in the framework of total algebras and first-order logic with equality. Received: 14 August 1995 / 1 April 1998     

Studies of a Theory of Specifications with Built-in Program Extraction

We present a Theory of Specifications based on Martin-Löf's type theory, with rules for simultaneously constructing programs and their correctness proofs. The theory contains types for representing specifications whose corresponding notion of implementation is that of a pair formed by a program and a correctness proof. The rules of the theory are such that in implementations the program parts appear mixed together with the proof parts. A confluent and normalizing computational relation performs the task of separating programs from proofs. As a consequence, every implementation computes to a pair composed of a program and a proof of its correctness, and so the program extraction procedure is immediate.     

Towards Acceptability of Optimizations: An Extended View of Compiler Correctness

The theory of relative program correctness and its preservation allows for elaborate and practically adequate definitions of correct implementation notions as they are established by transformations implemented in a compiler. It generalizes Hoare's and Floyd's partial and total program correctness and correctness preservation by classifying finite and infinite errors to be either acceptable (unavoidable) or unacceptable (chaotic, to be avoided). We will define correct implementation by particular compositional diagram commutativities, and we will further extend this theory also to express correctness of compiling specifications and of compiler programs and their implementations in the same uniform relational setting. Unacceptable error outcomes can semantically model pre-conditions such as well-formedness conditions for compilers or optimization pre-conditions for user programs. Our theory allows to distinguish between different correct implementation requirements, for instance (horizontally) for user programs or (vertically) for the compiler implementation, just as if we would switch on and off compiler options and tune one compiler to appropriately preserve correctness in different application domains.     

Systematic formal verification for fault-tolerant time-triggeredalgorithms

Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system and, then, to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems     

Abstract Implementation of Algebraic Specifications in a Temporal Logic Language

A formal technique for incorporating two specification paradigms is presented,in which an algebraic specification is implemented by a set of abstract procedures specified in pre and post-condition style.The link between the two level specifications is provided via a translation from terms of algebraic specifications into temporal logic formulae representing abstract programs.In terms of translation,a criterion for an abstract implementation satisfying its specification is given,which allows one to check the consistency between the two levels of specifications.The abstract implementations can be refined into executable code by refining each abstract procedure in it.It is proved that the satisfication relation between a specification and its implementations is preserved by such refinement steps.     

Engineering and analysis of fixed priority schedulers

Scheduling theory holds great promise as a means to a priori validate timing correctness of real-time applications. However, there currently exists a wide gap between scheduling theory and its implementation in operating system kernels running on specific hardware platforms. The implementation of any particular scheduling algorithm introduces overhead and blocking components which must be accounted for in the timing correctness validation process. This paper presents a methodology for incorporating the costs of scheduler implementation within the context of fixed priority scheduling algorithms. Both event-driven and timer-driven scheduling implementations are analyzed. We show that for the timer-driven scheduling implementations the selection of the timer interrupt rate can dramatically affect the schedulability of a task set, and we present a method for determining the optimal timer rate. We analyzed both randomly generated and two well-defined task sets and found that their schedulability can be significantly degraded by the implementation costs. Task sets that have ideal breakdown utilization over 90% may not even be schedulable when the implementation costs are considered. This work provides a first step toward bridging the gap between real-time scheduling theory and implementation realities. This gap must be bridged for any meaningful validation of timing correctness properties of real-time applications     

IPv6中Neighbor Discovery协议及其测试

IPv6协议是下一代互联网协议,NeighborDiscovery(邻居发现)协议是IPv6协议的一个重要组成部分,RFC2461是邻居发现协议的标准文本。为了检查各个生产厂家的实现是否与标准文本相一致,文章提出了一种协议一致性测试的方法,并开发了一个进行IPv6一致性测试的系统。该文提出了逻辑测试结构和虚拟测试器的概念,并在这个测试系统中应用了这两种测试结构和概念,还给出了一个邻居发现协议的测试实例。最后,给出了笔者对一种UNIX系统上实现的邻居发现协议进行一致性测试得到的结果,并对其与标准文本不一致的部分进行了分析说明。     

受损多智能体系统的信息一致性

针对受损多智能体系统的信息一致性问题, 基于代数图论提出了联合r连通概念, 给出了当系统中的部分成员受损或离开后不能继续原有工作时, 其余成员仍可实现一致性的充要条件. 研究结果表明, 在此条件下系统可失去成员的数量取决于系统的通信能力. 仿真实例验证了理论分析结果的正确性和有效性.     

Algebraic computational models of OR-parallel execution of Prolog

A specification of the OR-parallel execution of Prolog programs, using CHOCS (calculus of higher order communicating systems) [24], is presented in the paper. A translation is defined from Prolog programs and goals to CHOCS processes: the execution of the CHOCS process corresponding to a goal mimics the OR-parallel execution of the original Prolog goal. In the translation, clauses and predicate definitions of a Prolog program correspond to processes. To model OR-parallelism, the processes , corresponding to clauses (having the same head predicate ) start their execution concurrently, but, in order to respect the depth-first search rule, each is guarded by the termination of the executions of processes 's, . The computational model is proved correct with respect to the semantics of Prolog, as given in [4, 5]. Our model, because of its algebraic specification, can be easily used to prove properties of the parallel execution of Prolog programs. Moreover, the model exploits the maximum degree of parallelism, by giving the Prolog solutions in parallel, without any order among them. However, this model, being close to the Prolog semantics definition, contains sources of inefficiency which make it unpractical as a guide for the implementation. To overcome these problems, a new computational model is defined. This model is obtained by modifications of the basic one and thus its correctness can be easily proved. Finally, we show how to obtain models of different real implementations of OR-parallel Prolog by slight modification of the new model. The relations among all these models, in terms of parallelism degree, are studied by using the concepts of bisimulation and simulation, developed for concurrent calculi. Received: 5 May 1995 / 28 May 1996     

利用增量矩阵辨识确定型ARMA模型的新算法

本文提出了一种无偏辨识确定型ARMA模型参数及阶次的新方法。和其他辨识算法不同的是在这里我们构造了关于系统开环阶跃响应的增量矩阵,并且通过分析该增量矩阵子矩阵的代数性质而得到了辨识系统阶次的一种简单方法。仿真的结果说明了本文理论的正确性。     

Formal testing from timed finite state machines

In this paper we present a formal methodology to test both the functional and temporal behaviors in systems where temporal aspects are critical. We extend the classical finite state machines model with features to represent timed systems. Our formalism allows three different ways to express the timing requirements of systems. Specifically, we consider that time requirements can be expressed either by means of fix time values, by using random variables, or by considering time intervals. Different implementation relations, depending on both the interpretation of time and on the non-determinism appearing in systems, are presented and related. We also study how test cases are defined and applied to implementations. Test derivation algorithms, producing sound and complete test suites, are also presented. That is, by deriving these test suites we relate the different notions of passing tests and the different implementation relations. In other words, for a given correctness criterion, a system represents an appropriate implementation of a given model if and only if the system successfully passes all the test belonging to the derived test suite.     

以操作系统为中心的存储一致性模型--线程一致性模型

分布共享存储系统为保证程序的正确执行，必须通过存储一致性模型对共享存储访问顺序加以限制，而现有模型在可扩展性和操作系统级实现方面存在不足。结合多线程的特点，提出了一种以操作系统为中心的线程一致性模型，通过并行程序执行过程中线程状态的变化来观察和限制存储访问事件的正确顺序，有利于系统的可扩展性、一致性维护信息获取的方便性和完备性以及操作系统本身的设计和实现。分别从模型的定义、正确性证明、实现方案和性能分析等几个方面展开了论述。     

Observational implementation of algebraic specifications

Summary An observational approach to the construction of implementations of algebraic specifications is presented. Based on the theory of observational specifications an implementation relation is defined which formalizes the intuitive idea that an implementation is correct if it produces correct observable output. To be useful in practice proof theoretic criteria for observational implementations are provided and a proof technique (called context induction) for the verification of implementation relations is presented. As an example an abstract specification of (the algebraic semantics of) a small imperative programming language is implemented by a state oriented specification of the language.In order to support the modular construction of implementations the approach is extended to parameterized observational specifications. Based on the notion of observable parameter context a proof theoretic criterion for parametrized observational implementations is presented and it is shown that under appropriate conditions observational implementations compose horizontally. The given implementation criteria are applied to examples.     

一种AES S盒改进方案及其硬件设计

为提高高级加密标准（advanced encryption standard,AES）算法的安全性,提出了一种新的S盒生成方案。在分析了现有S盒存在的问题后,基于S盒的构造原理和密码学性质,通过选择新的不可约多项式和仿射变换对,同时调整仿射变换与乘法逆的运算顺序,构造出一种新的S盒;对生成的新S盒与AES 的S盒以及其他改进S盒在代数式项数、严格雪崩标准距离等方面进行了比较,结果显示新S盒具有更好的代数性质,能够有效抵御代数攻击;还对新S盒进行了硬件设计并优化,DC综合结果显示新S盒复域优化实现消耗的资源比传统复域实现少12%,比查找表法实现少41%。新S盒在安全性方面优于现有S盒,将其应用于AES软件设计和硬件设计,并通过仿真测试验证了其正确性。     

A Problem-Reduction Approach to Proving Simulation Between Programs

System correctness often presents itself as the problem of showing that two programs, the "specification" and the "implementation," are in some sense equivalent. Such a concept of equivalence is supplied by Milner's definition of simulation between programs. This paper presents a problem-reduction approach to proving simulation, and describes an interactive system designed for this purpose.     

Fast bio-inspired computation using a GPU-based systemic computer

Biology is inherently parallel. Models of biological systems and bio-inspired algorithms also share this parallelism, although most are simulated on serial computers. Previous work created the systemic computer – a new model of computation designed to exploit many natural properties observed in biological systems, including parallelism. The approach has been proven through two existing implementations and many biological models and visualizations. However to date the systemic computer implementations have all been sequential simulations that do not exploit the true potential of the model. In this paper the first ever parallel implementation of systemic computation is introduced. The GPU Systemic Computation Architecture is the first implementation that enables parallel systemic computation by exploiting the multiple cores available in graphics processors. Comparisons with the serial implementation when running two programs at different scales show that as the number of systems increases, the parallel architecture is several hundred times faster than the existing implementations, making it feasible to investigate systemic models of more complex biological systems.     

Design principles for motion control system software

The paper examines issues associated with the concept of development of software of motion control systems intended for processing unit automation. Possible variants of hardware and software implementation of such systems are given. The concept for building the motion control system on the basis of automaton-based realization of logical control and motion control programs (PLC and PMC) via the virtual machine is proposed. The Forth implementation of automaton-based programming of PLC programs is demonstrated.     

Deriving real-time action systems with multiple time bands using algebraic reasoning

The verify-while-develop paradigm allows one to incrementally develop programs from their specifications using a series of calculations against the remaining proof obligations. This paper presents a derivation method for real-time systems with realistic constraints on their behaviour. We develop a high-level interval-based logic that provides flexibility in an implementation, yet allows algebraic reasoning over multiple granularities and sampling multiple sensors with delay. The semantics of an action system is given in terms of interval predicates and algebraic operators to unify the logics for an action system and its properties, which in turn simplifies the calculations and derivations.