检索结果-内蒙古大学图书馆

8th Workshop on Parallel and Distributed Simulation, PADS 1994

作者： Wood, Kenneth R. Turner, Stephen J. Programming Research Group Oxford University Computing Laboratory United Kingdom Department of Computer Science University of Exeter United Kingdom

ISBN: (纸本)1565550277

The carrier-null message approach to conservative distributed discrete-event simulation can significantly reduce the number of synchronization messages required to avoid deadlock. In thts paper we show that the original approach does not apply to simulations with arbitrary communication graphs and we propose a modified carrier-null approach whtch does. We present and discuss some preliminary results obtained using our approach to simulate digital logic circuits.

关键词： Discrete event simulation

来源：评论

学校读者我要写书评

暂无评论

Categories, Relations and Dynamic programming

引用

Mathematical Structures in Computer Science 1994年第1期4卷 33-69页

作者： De Moor, Oege Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD 11 Keble Road United Kingdom

Dynamic programming is a strategy for solving optimisation problems. In this paper, we show how many problems that may be solved by dynamic programming are instances of the same abstract specification. This specification is phrased using the calculus of relations offered by topos theory. The main theorem underlying dynamic programming can then be proved by straightforward equational *** generic specification of dynamic programming makes use of higher-order operators on relations, akin to the fold operators found in functional programming languages. In the present context, a data type is modelled as an initial F-algebra, where F is an endofunctor on the topos under consideration. The mediating arrows from this initial F-algebra to other F-algebras are instances of fold – but only for total functions. For a regular category ε, it is possible to construct a category of relations Rel(ε). When a functor between regular categories is a so-called relator, it can be extended (in some canonical way) to a functor between the corresponding categories of relations. Applied to an endofunctor on a topos, this process of extending functors preserves initial algebras, and hence fold can be generalised from functions to *** is well-known that the use of dynamic programming is governed by the principle of optimality. Roughly, the principle of optimality says that an optimal solution is composed of optimal solutions to subproblems. In a first attempt, we formalise the principle of optimality as a distributivity condition. This distributivity condition is elegant, but difficult to check in practice. The difficulty arises because we consider minimum elements with respect to a preorder, and therefore minimum elements are not unique. Assuming that we are working in a Boolean topos, it can be proved that monotonicity implies distributivity, and this monotonicity condition is easy to verify in practice.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Specification, Verification and Prototyping of an Optimized Compiler

引用

Formal Aspects of Computing 1994年第6期6卷 643-658页

作者： Jifeng, He Bowen, Jonathan Oxford University Computing Laboratory Programming Research Group Oxford OX1 3QD Wolfson Building Parks Road United Kingdom

This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optimization issues of concern here include the use of existing contents of registers where possible and the identification of common expressions. A register table is introduced in the compiling specification predicates to map each register to an expression whose value is held by it. We define different kinds of predicates to specify compilation of programs, expressions and Boolean tests. A set of theorems relating to these predicates, acting as a correct compiling specification, are presented and an example proof within the refinement algebra of the programming language is given. Based on these theorems, a prototype compiler in Prolog is produced. © 1994 BCS.

关键词： Code optimization Formal verification Logic programming Program compilation Refinement algebra

来源：评论

学校读者我要写书评

暂无评论

Towards a provably correct compiler for OBJ3 6th

Towards a provably correct compiler for OBJ3

引用

6th International Symposium on programming Language Implementation and Logic programming, PLILP 1994

作者： Hamel, Lutz H. Goguen, Joseph A. Programming Research Group Oxford University Computing Laboratory Oxford0X1 3QD United Kingdom

ISBN: (纸本)9783540584025

Machines have proved very successful in the implementation of very high level logic and functional programming languages;in particular, we have the G-machine for functional programming languages and the WAM for Prolog. In this paper we develop an abstract machine appropriate for the implementation of algebraic specification languages. We then employ general algebra techniques and initiality properties to prove correctness of the translation from equational rewrite rules to the abstract machine code. The correctness proof itself has been automated using the 0BJ3 system. © Springer-Verlag Berlin Heidelberg 1994.

关键词： Algebra

来源：评论

学校读者我要写书评

暂无评论

Case study: Specification and refinement of the PI-Bus 2nd

引用

2nd International Symposium of Formal Methods Europe, FME 1994

作者： Seidel, Karen Oxford University Computing Laboratory Programming Research Group Wolfson Building Parks Road OxfordOX1 3QD United Kingdom

ISBN: (纸本)9783540585558

The Peripheral Interconnect Bus (PI-Bus) is part of the Open Microprocessor systems Initiative, which is in the process of setting standards for a wide range of chip components, so as to guarantee compatibility between components from different vendors. One of the problems arising in the standardization effort is that the standard needs to be as definite as possible without prejudicing implementation issues. This paper presents a formalisation of the draft standard for the PI-Bus which suggests that this problem has not yet been adequately addressed. We use CSP to give a high-level specification which corresponds to the compulsory aspects of the draft standard, and show that there are two implementations which are both valid refinements of the specification, but are mutually incompatible. Explicit timing events are used to bound to the nearest clock phase the time at which a communication event may happen and avoid the necessity to reason in a fully timed semantics. There is, however, a slight deviation from standard CSP in that choice between communication and timing events is prioritised towards the former. This means that a process will perform a communication event rather than a timing event whenever it has the choice. © 1994, Springer Verlag. All rights reserved.

关键词： Specifications

来源：评论

学校读者我要写书评

暂无评论

Towards a declarative framework for hardware-software codesign 94

Towards a declarative framework for hardware-software codesi...

引用

International Workshop on Hardware/Software Codesign (CODES)

作者： W. Luk T. Wu Programming Research Group Oxford University Computing Laboratory Oxford UK

ISBN: (纸本)9780818663154

We present an experimental framework for mapping declarative programs, written in a language known as Ruby, into various combinations of hardware and software. Strategies for parametrised partitioning into hardware and software can be captured concisely in this framework, and their validity can be checked wing algebraic reasoning. The method has been used to guide the development of prototype compilers capable of producing, from a Ruby expression, a variety of implementations involving field programmable gate arrays (FPGAs) and microprocessors. The viability of this approach is illustrated using a number of examples for two reconfigurable systems, one containing an array of Algotronix devices and a PC host, and the other containing a transputer and a Xilinx device.< >

关键词： Software tools Field programmable gate arrays Process design Laboratories Software prototyping Prototypes Program processors Microprocessors Hardware design languages Signal design

来源：评论

学校读者我要写书评

暂无评论

Hardware-software codesign of multidimensional programs

Hardware-software codesign of multidimensional programs

引用

IEEE Workshop on FPGAs for Custom Computing Machines

作者： W. Luk T. Wu I. Page Programming Research Group Oxford University Computing Laboratory Oxford UK

Presents a method for parametrised partitioning of multidimensional programs for acceleration using a hardware coprocessor. The method involves a divide-and-conquer structure, with the "divide" and "merge" phases carried out by a general-purpose processor, while the "conquer" phase is handled by application-specific hardware. The partitioning strategy has been captured in a simple functional language, and we have automated the production of partitioned programs in this language. Our approach has been tested on an FPGA-based system using a number of computer vision algorithms, including the Canny edge detector, and the performance is compared against executing the programs on the PC host.< >

关键词： Multidimensional systems Hardware Programmable logic arrays Computer vision Partitioning algorithms Field programmable gate arrays Laboratories Acceleration Coprocessors Software testing

来源：评论

学校读者我要写书评

暂无评论

A formal specification of an automatic train protection system 2nd

引用

2nd International Symposium of Formal Methods Europe, FME 1994

作者： Simpson, Andrew Programming Research Group Oxford University Computing Laboratory Wolfson Building OxfordOX1 3QD United Kingdom Smith Institute Surrey Research Park Guildford SurreyGU2 5YP United Kingdom

ISBN: (纸本)9783540585558

This paper attenlpts to provide a formed specification of an Automatic Train Protection (ATP) system. Such a system continuously checks the actual speed of a passenger train against its maximum permitted speed and takes appropriate action if it detects that the train is travelling too fast. We propose a Communicating Sequential Processes (CSP) specification of such a system and describe how the proof tool Failures Divergence Refinement (FDR) has been used to verify that our specification meets its requirements. © 1994, Springer Verlag. All rights reserved.

关键词： Formal specification

来源：评论

学校读者我要写书评

暂无评论

Calculation of the temperature distribution in an asynchronous machine

引用

European Transactions on Electrical Power 1995年第3期5卷 181-186页

作者： Xypteras, J. Maras, K. Spyrelis, D. Associate Professor Dr.-Ing. Jannis Xypteras (1937) Director of the Electrical Machines Laboratory Dept. of Electrical Engineering Aristotle University of Thessaloniki (AUT)/Greece graduated from the Fakultatfur Elektrotechnik of the RWTH AachedGermany. During the years 1965 to 1980 he had been employed in German and Greek factories for electrical machines several years as chief of development departments. In 1978 he obtained his Dr. Electr. Eng. degree in the AUT. His subject was in the area of eddy currents. Since 1984 he is Ass. hofessor in the same University. His special interests: Design and development of electrical machines vibration and noise problems electromagnetic fields eddy currents. (Dept. of Electrical Engineering Aristotle University GR-54006 Thessaloniki/Greece T +30 3 1 I99 62 93 Fax +303 11 99 63 02) Kostas Maras (1966) received his degree in Electrical Engineering from the Electrotechnical Faculty of Aristotle University of Thessaloniki/Greece in 1989. In 1990 he graduated as M.Sc. in Digital Electronics in the King's College London at the University of LondordGB with the project “Design of a Transversal Filter on VLSI CMOS”. Since then he has been working at M. Papasavas S.A. at KallithedGreece as an analyst in developing industrial software. Projects: Design and implementation of a dynamic relational model used to tackle production problems in industry. From 1991 to 93 he was responsible for the development of production planning used in industries. (M. Papasavas S.A. Sofocleus 261 GR-17874 KallithedGreece T +30 119423246 Fax +30 1/9429561) Dimitrios S. Spyrelis (1965) received his Diploma in Electrical Engineering from the University of Thessalonikil Greece in 1989. In 1990 he joined the Coding Center of Greek Army as research Assistant. He is currently working as technical director in a pigpoultry breeding company which includes feed processing industry slaughter houses by product process industry wastes treatment systems from farm livestock. His last fields of interest

In this paper the temperature distribution on the section vertical to the axis of an asynchronous machine is calculated. For the calculation the numerical method of “Control Volumes” has been used. The technique used can be easily modified to fit any kind of machine. It can also analyse transients. Copyright © 1995 John Wiley & Sons, Ltd.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Retargeting a hardware compiler proof using protocol converters

Retargeting a hardware compiler proof using protocol convert...

引用

International Symposium on Advanced research in Asynchronous Circuits and Systems

作者： G. Brown W. Luk J. O'Leary School of Electrical Engineering Cornell University Ithaca NY USA Programming Research Group Computing Laboratory Oxford University Oxford UK

We show how to retarget the correctness proof of a hardware compiler generating two-phase delay-insensitive circuits to a compiler generating four-phase speed-independent circuits. We use protocol converters to convert the specifications of our compiler's two-phase circuit elements into equivalent specifications for four-phase elements. The processes of converting the specifications and verifying their implementations are automated.

关键词： Hardware Protocols Delay Asynchronous circuits Production Program processors Laboratories Buildings Europe System recovery

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：