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

2001 ASEE Annual Conference and Exposition: Peppers, Papers, Pueblos and Professors

作者： Head, Linda Kay, Jennifer Schmalzel, John Arr, Glenn Foster, Christopher McDermott, Steven Sterner, Michael Whelan, Kenneth Wollenberg, Jason Department of Electrical Engineering Rowan University 201 Mullica Hill Rd. Glassboro NJ 08028 Department of Computer Science Rowan University 201 Mullica Hill Rd. Glassboro NJ 08028 ECE Student Teaching Team Rowan University 201 Mullica Hill Rd. Glassboro NJ 08028

THe initiation of a Programming Preparation Course for enhancing students' preparation in a C++ programming course and their level of confidence in mastering the basics of computer programming is discussed. The course is a collaborative effort of faculty in the College of Engineering and the computer science department. The topics used to introduce the fundamentals of programming include variables, loops and input, and function calls. The instructor team that has developed thsi course has the potential of increasing student retention in the programming course during the spring semester.

关键词： Engineering education

来源：评论

学校读者我要写书评

暂无评论

On-the-fly conformance testing using SPIN

引用

International Journal on Software Tools for Technology Transfer 2000年第4期2卷 382-393页

作者： de Vries, René G. Tretmans, Jan University of Twente Department of Computer Science Formal Methods and Tools Group P.O. Box 217 7500 AE Enschede Netherlands

In this paper we report on the construction of a tool for conformance testing based on Spin. The Spin tool has been adapted such that it can derive the building blocks for constructing test cases, called test primitives, from systems described in Promela. The test primitives support the on-the-fly conformance testing process. Traditional derivation of tests from formal specifications suffers from the state-space explosion problem. Spin is one of the most advanced model checkers with respect to handling large state spaces. This advantage of Spin has been used for the derivation of test primitives from a Promela description. To reduce the state space, we introduce the on-the-fly testing framework. One of the components within this framework is the Primer. The Primer is responsible for deriving test primitives from a model of a system according to a well-defined and complete testing theory. Algorithms are presented which enable us to derive test primitives from a Promela description. These algorithms have been implemented in the adapted version of the Spin tool which acts as the Primer in the framework. Promising experiments have been carried out on an example case study. As a result of this study it is concluded that it is possible to derive test primitives automatically from Promela descriptions, construct test cases from these test primitives, and execute the test cases on-the-fly. © 2000 Springer-Verlag.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Visualizing system factorizations with behavior tables 3rd

引用

3rd International Conference on Formal methods in computer-Aided Design, FMCAD 2000

作者： Tsow, Alex Johnson, Steven D. System Design Methods Laboratory Computer Science Department Indiana University United States

ISBN: (纸本)3540412190

Behavior tables are a design formalization intended to support interactive design derivation for hardware and embedded systems. It is a reformulation of the DDD transformation system, bridging behavioral and architectural forms of expression. The tabular representations aid in visualizing design aspects that are subject to interactive refinement and optimization. These ideas are illustrated for system factorization, an import class of decompositions used in design derivation. A series of examples shows how features seen in the behavior tables determine the course of a factorization and how the rules of a core behavior table algebra compose into the more large scale transformations done at the interactive level. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Factorization

来源：评论

学校读者我要写书评

暂无评论

Verification is experimentation!

Verification is experimentation!

引用

11th International Conference on Concurrency Theory, CONCUR 2000

作者： Brinksma, Ed Department of Formal Methods and Tools Faculty of Computer Science University of Twente PO Box 217 7500AE Enschede Netherlands

ISBN: (纸本)3540678972

The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer aided formal verification. They are making formal verification a practical proposition for a growing class of real-life applications, and have put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigm in at least two senses. We submit that this observation has consequences for the ways in which we should research and apply formal methods. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

Parallel access to persistent multidimensional arrays from HPF applications using Panda 8th

引用

8th International Conference on High Performance Computing and Networking, HPCNEurope 2000

作者： Brezany, Peter Czerwiński, Przemys Law Świętanowski, Artur Winslett, Marianne Institute for Software Science University of Vienna Liechtensteinstrasse 22 ViennaA-1090 Austria Department of Statistics Operations Research and Computer Methods University of Vienna Universitätsstrasse 5 ViennaA-1010 Austria Database Research Laboratory Department of Computer Science University of Illinois 1304 W. Springfield UrbanaIL61801 United States

ISBN: (纸本)9783540675532

A critical performance issue for a number of scientific and engineering applications is the eficient transfer of data to secondary storage. Languages such as High Performance Fortran (HPF) have been introduced to allow programming distributed-memory systems at a relatively high level of abstraction. However, the present version of HPF does not provide appropriate constructs for controlling the parallel I/O capabilities of these systems. In this paper, constructs to specify parallel I/O operations on multidimensional arrays in the context of HPF are proposed. The paper also presents implementation concepts that are based on the HPF compiler developed at the University of Vienna and the parallel I/O runtime system Panda developed at the University of Illinois. Experimental performance results are discussed in the context of financial management and traffic simulation applications. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Data transfer

来源：评论

学校读者我要写书评

暂无评论

Using active server pages and simulation techniques to create virtual M&M's 00

Using active server pages and simulation techniques to creat...

引用

Proceedings of the fourteenth annual consortium on Small Colleges Southeastern conference

作者： Robin M. Snyder Department of Computer Science and Quantitative Methods College of Business Administration Winthrop University Rock Hill SC

The M&M problem is an excellent example of a nontrivial yet simple method for summarizing sampled data that are then used in making decisions. Simulating the creation of virtual M&M's that can be copied and pasted into a spreadsheet as the raw data for the M&M problem provides a way for students to get a unique sample of M&M's, thus modeling how, in an information systems environment, sampled raw data can often be captured electronically rather than being entered by hand as would be the case with a physical package of M&M's. Previously presented using client-side JavaScript, this paper presents a solution to the same problem using server-side Active Server Pages, thus avoiding compatibility problems of client-side scripting. The paper serves as a short introduction to both programming in Active Server Pages and to simulating discrete events.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A method using procedural parameters and callback functions to create a generic exchange-sorting module 00

A method using procedural parameters and callback functions ...

引用

Proceedings of the fourteenth annual consortium on Small Colleges Southeastern conference

作者： Robin M. Snyder Department of Computer Science and Quantitative Methods College of Business Administration Winthrop University Rock Hill SC

A generic exchange-sorting module obviates the need for duplicating sort code in a program, thus promoting module reuse. This paper presents a method for using procedural parameters and callback functions to create a generic exchange-sorting module. Based on techniques with roots in functional programming using higher order functions, the method is fairly easy to understand. More importantly it is easy to use, even for beginning programmers. Using the rapid application development system Delphi and it's Object Pascal programming language, the method is presented in a way that highlights some useful features of Object Pascal that might not be well known to readers more familiar with the now-outdated standard Pascal or the currently popular C++.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Risk bands-a novel feature of Safecharts

Risk bands-a novel feature of Safecharts

引用

International Symposium on Software Reliability Engineering (ISSRE)

作者： N. Nissanke H.Z. Dammag Department of Computer Science University of Reading Reading UK Centre for Applied Formal Methods School of Computing South Bank University London UK

Safecharts (H. Dammeg and N. Nissanke, 1999) are a safety oriented variant of Statecharts (D. Harel, 1987) and have been developed especially for the use in specification and design of safety critical systems. One of the fundamental aspects of Safecharts is the explicit ordering of system states according to their risk levels. Based on this ordering, transitions are classified according to the nature of their risk and are given a priority scheme favouring the execution of safer transitions in the event of any nondeterminism. As a precaution, transitions between states with unknown relative risk levels are not permitted. As a result, many transitions, including those which might be functionally desirable, may be potentially excluded between states which are located in sparsely populated areas of risk graphs. This is an inadequacy which may be attributed to factors such as incomplete hazard analysis, the lack of information about relative risk levels of different states of the system, etc. In order to extend the permitted transition space in such circumstances and to enhance the risk ordering relation, the paper introduces the concept of risk band. Risk bands enable an unambiguous interpretation of the relevant risk level of states, thus allowing a well understood enhancement of risk graphs and an extension of the concept of safe non-determinism introduced by H. Dammeg and N. Nissanke (1999). An example drawn from the nuclear industry demonstrates the application of Safecharts.

关键词： Safety State-space methods Information systems Mathematics Hazards Information analysis Risk analysis Communication industry Industrial relations Application software

来源：评论

学校读者我要写书评

暂无评论

An integrated CSP-based tool for the visualisation, animation and performance evaluation of message passing algorithms

An integrated CSP-based tool for the visualisation, animatio...

引用

International Conference on Formal Engineering methods

作者： A.E. Abdallah M. Green Centre for Applied Formal Methods School of Computing Information and Mathematics South Bank University London UK Department of Computer Science University of Reading Reading UK

This paper presents ongoing research and development on an integrated tool for the visualisation and animation of message-passing communicating systems described in Hoare's CSP (Communicating Sequential Processes). It introduces major new developments to the original VisualNets implemented in C++ and reported in (Abdallah, 1998). The new tool is implemented partly in Java and partly in the functional programming language Haskell. Not only does the new tool enjoy greater expressive power and a better user interface, it has new capabilities for aiding the user in animating, analysing and reasoning about CSP specifications. These include provisions for nested parallelism within a single node, improved profiling and animation, and the possibility of applying generic timing cost models for performance evaluation. The paper briefly describes the new features, explains the methods by which they have been implemented and illustrates their use with examples.

关键词： Visualization Animation Message passing Java Formal specifications Mathematics computer science Research and development Parallel processing Timing

来源：评论

学校读者我要写书评

暂无评论

Restarts can help in the on-line minimization of the maximum delivery time on a single machine

Restarts can help in the on-line minimization of the maximum...

引用

8th Annual European Symposium on Algorithms, ESA 2000

作者： Van Den Akker, Marjan Hoogeveen, Han Vakhania, Nodari Department of Mathematical Models and Methods National Aerospace Laboratory NLR P.O. Box 90502 Amsterdam1006 BM Netherlands Department of Computer Science Utrecht University P.O. Box 80089 UtrechtTB3508 Netherlands State University of Morelos FC Ueam AV. Universidad 1001 CuernavacaMor62210 Mexico

ISBN: (纸本)354041004X

We consider a single-machine on-line scheduling problem where jobs arrive over time. A set of independent jobs has to be scheduled on a single machine. Each job becomes available at its release date, which is not known in advance, and its characteristics, i.e., processing requirement and delivery time, become known at its arrival. The objective is to minimize the time by which all jobs have been delivered. In our model preemption is not allowed, but we are allowed to restart a job, that is, the processing of a job can be broken off to have the machine available to process an urgent job, but the time already spent on processing this interrupted job is considered to be lost. We propose an on-line algorithm and show that its performance bound is equal to 1.5, which matches a known lower bound due to Vestjens. For the same problem without restarts the optimal worst-case bound is known to be equal to (√ 5 + 1)/2 ≈ 1.61803;this is the first example of a situation in which the possibility of applying restarts reduces the worst-case performance bound, even though the processing times are known. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Scheduling algorithms

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：