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

General distributions in process algebra 1st

1st EEF/Euro Summer School on Formal methods and Performance Analysis, FMPA2000

作者： Katoen, Joost-Pieter D’Argenio, Pedro R. Formal Methods and Tools Group Dept. of Computer Science University of Twente P.O. Box 217 Enschede7500 AE Netherlands

ISBN: (纸本)3540424792

This paper is an informal tutorial on stochastic process algebras, i.e., process calculi where action occurrences may be subject to a delay that is governed by a (mostly continuous) random variable. Whereas most stochastic process algebras consider delays determined by negative exponential distributions, this tutorial is concerned with the integration of general, non-exponential distributions into a process algebraic setting. We discuss the issue of incorporating such distributions in an interleaving semantics, and present some existing solutions to this problem. In particular, we present a process algebra for the specification of stochastic discrete-event systems modeled as generalized semi-Markov chains (GSMCs). Using this language stochastic discrete-event systems can be described in an abstract and modular way. The operational semantics of this process algebra is given in terms of stochastic automata, a novel mixture of timed automata and GSMCs. We show that GSMCs are a proper subset of stochastic automata, discuss various notions of equivalence, present congruence results, treat equational reasoning, and argue how an expansion law in the process algebra can be obtained. As a case study, we specify the root contention phase within the standardized IEEE 1394 serial bus protocol and study the delay until root contention resolution. An overview of related work on general distributions in process algebra and a discussion of trends and future work complete this tutorial. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Markov processes

来源：评论

学校读者我要写书评

暂无评论

CardS4: Modal theorem proving on java smartcards

引用

International Conference on Research in Smart Cards, E-smart 2001

作者： Goré, Rajeev Prabhakar Nguyên, Phuong Thê Automated Reasoning Group Computer Sciences Laboratory Res. Sch. of Inf. Sci. and Eng Institute of Advanced Studies Australian National University Australia Formal Methods Group Dept. of Computer Science Inf. Tech Australian National University Australia

ISBN: (纸本)3540426108

We describe a successful implementation of a theorem prover for modal logic S4 that runs on a Java smart card with only 512 KBytes of RAM and 32KBytes of EEPROM. Since proof search in S4 can lead to infinite branches, this is "proof of principle" that non-trivial modal deduction is feasible even on current Java cards. We hope to use this prover as the basis of an on-board security manager for restricting the flow of "secrets" between multiple applets residing on the same card, although much work needs to be done to design the appropriate modal logics of "permission" and "obligations". Such security concerns are the major impediments to the commercial deployment of multi-application smart cards. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Smart cards

来源：评论

学校读者我要写书评

暂无评论

Faster and symbolic ctmc model checking 1st

Faster and symbolic ctmc model checking

引用

1st Joint International Workshop on Process Algebras and Performance Modeling and Probabilistic methods in Verification, PAPM-PROBMIV 2001

作者： Katoen, Joost-Pieter Kwiatkowska, Marta Norman, Gethin Parker, David Formal Methods and Tools Group University of Twente P.O. Box217 Enschede7500 AE Netherlands School of Computer Science University of Birmingham Edgbaston BirminghamB15 2TT United Kingdom

ISBN: (纸本)354042556X

This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N) in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Extreme interleavings

引用

IEEE Distributed Systems Online 2001年第1期2卷

作者： Ben-Ari, Mordechai Burns, Alan Weizmann Institute of Science Israel University of York United Kingdom Dept. of Science Teaching Weizmann Inst. of Science Rehovot 76100 Israel Dept. of Computer Science Univ. of York Heslington York YO1 5DD United Kingdom

The use of concurrency simulators for teaching concurrent programming is discussed. A concurrency simulator is better than a standard concurrent language for introductory courses, as it provides fine-grained control over process scheduling. An example of a concurrent program and its results in a concurrent simulator are also given. The interleaving of all iterations in the program are also presented.

关键词： computer programming

来源：评论

学校读者我要写书评

暂无评论

Building confidence and skills: A prep course for computer programming

Building confidence and skills: A prep course for computer p...

引用

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

来源：评论

学校读者我要写书评

暂无评论

Designing and implementing active learning in the computer science curriculum: an interactive tutorial

Journal of Computing Sciences in Colleges

引用

Journal of Computing sciences in Colleges 2001年第2期17卷

作者： D. V. Pigford Professor of Computer Science Faculty Associate Center for Teaching and Learning Western Kentucky University Bowling Green KY

This paper/tutorial is designed to introduce participants to a variety of activity-based, cooperative techniques [1], [2], [8], [9] for enhancing learning and promoting assessment in the computer science curriculum. Six different active learning structures for achieving increased student involvement and professor assessment of outcomes [1] will be explained and demonstrated with audience participation. The advantages, disadvantages, flexibility, timing,@labor costs@, and sequencing of these techniques will be highlighted. Examples of using each of the six methods will be taken from actual classroom materials/practices used by the author in an Oracle based senior database class, a programming language course, a junior software engineering class, and an introductory structured programming class for non-majors.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Task rearrangement on partially reconfigurable FPGAs with restricted buffer 10th

引用

10th International Conference on Field-Programmable Logic and Applications, FPL 2000

作者： Elgindy, Hossam Middendorf, Martin Schmeck, Hartmut Schmidt, Bernd School of Computer Science and Engineering University of New South Wales Sydney2052 Australia Institute of Applied Computer Science and Formal Description Methods University of Karlsruhe KarlsruheD-76128 Germany

ISBN: (纸本)3540678999

Partially reconfigurable FPGAs can be shared among multiple independent tasks. When partial reconfiguration is possible at runtime the FPGA controller can decide on-line were to place new tasks on the FPGA. Since on–line allocation suffers from fragmentation, tasks can end up waiting despite there being sufficient, albeit non–contiguous resources available to service them. Rearranging a subset of the tasks executing on the FPGA often allows the next pending task to be processed sooner. In this paper we study the problem of placing and rearranging tasks that are supplied by input streams which have constant data rates. When such tasks are rearranged, the arriving input data have to be buffered while the execution is suspended. We describe and evaluate a genetic algorithm for identifying and scheduling feasible rearrangements when moving tasks are reloaded from off–chip and buffer size is limited. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Field programmable gate arrays (FPGA)

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：