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

11th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2005, held as part of the Joint European conferences on theory and Practice of Software, ETAPS 2005

作者： Bingham, Jesse Hu, Alan J. Department of Computer Science University of British Columbia Canada

Well-structured transition systems (WSTS) are a broad and well-studied class of infinite-state systems, for which the problem of verifying the reachability of an upward-closed set of error states is decidable (subject to some technicalities). Recently, Bingham proposed a new algorithm for this problem, but applicable only to the special cases of broadcast protocols and petri nets. the algorithm exploits finite-state symbolic model checking and was shown to outperform the classical WSTS verification algorithm on a contrived example family of petri nets. In this work, we generalize the earlier results to handle a larger class of WSTS, which we dub nicely sliceable, that includes broadcast protocols, petri nets, context-free grammars, and lossy channel systems. We also add an optimization to the algorithm that accelerates convergence. In addition, we introduce a new reduction that soundly converts the verification of parameterized systems with unbounded conjunctive guards into a verification problem on nicely sliceable WSTS. the reduction is complete if a certain decidable side condition holds. this allows us to access industrially relevant challenge problems from parameterized memory system verification. Our empirical results show that, although our new method performs worse than the classical approach on small petri net examples, it performs substantially better on the larger examples based on real, parameterized protocols (e.g., German's cache coherence protocol, with data paths). © Springer-Verlag Berlin Heidelberg 2005.

关键词： Finite automata

来源：评论

学校读者我要写书评

暂无评论

Rewriting tables and memorized semirings

Rewriting tables and memorized semirings

引用

IEEE international conference on Electronics, Circuits and systems (ICECS)

作者： Gerard H.E. Duchamp Khalaf Khatatneh Cyrille Bertelle Institut Galilée University of Paris XIII Villetaneuse France Al-Balqa-Applied University Al-Salt Jordan LIH University of Le Havre Le Havre France

the following is intended to be a contribution in the area of what could be called efficient algebraic structures or efficient data structures. In fact, we define and construct a new data structure, the tables (abstract and reduced), which are at first special multisets of two-raws arrays. the first raw is filled with words (or more generally, elements taken in some semigroup) and the second with some coefficients taken in a semiring.

关键词： Automata Convolution Adaptation models Finite element analysis Computational modeling Algebra tools

来源：评论

学校读者我要写书评

暂无评论

Control algorithms for active relative motion cancelling for robotic assisted off-pump coronary artery bypass graft surgery

Control algorithms for active relative motion cancelling for...

引用

international conference on Advanced Robotics (ICAR)

作者： M.C. Cavusoglu J. Rotella W.S. Newman Sangeun Choi J. Ustin S.S. Sastry Department of Electrical Engineering and Computer Science Case Western Reserve University Cleveland OH USA School of Medicine Emory University Atlanta GA USA Department of Electrical Engineering and Computer Sciences University of California Berkeley CA USA

Use of intelligent robotic tools promises an alternative and superior way of performing off-pump coronary artery bypass graft (CABG) surgery. In the robotic-assisted surgical paradigm proposed, the conventional surgical tools are replaced with robotic instruments which are under direct control of the surgeon through teleoperation. the robotic tools actively cancel the relative motion between the surgical instruments and the point-of-interest on the beating heart, in contrast to traditional off-pump CABG where the heart is passively constrained to dampen the beating motion. As a result, the surgeon operates on the heart as if it were stationary. We call the proposed algorithm "active relative motion cancelling (ARMC)" to emphasize the active cancellation. In the paper, a model-based intelligent ARMC algorithm is proposed to achieve effective motion cancellation. this is followed by an analysis of local motion of the heart collected using a sonomicrometry system to determine the specifications for ARMC system. Finally, the experimental results of the algorithm implemented on two 1-DOF robotic test-bed systems are reported

关键词： Motion control Arteries Surgery Heart Surgical instruments Surges Intelligent robots Tracking Robot vision systems Cameras

来源：评论

学校读者我要写书评

暂无评论

Embedded system engineering using C/C++ based design methodologies

Embedded system engineering using C/C++ based design methodo...

引用

international conference and Workshop on Engineering of Computer-Based systems

作者： C. Talarico Aseem Gupta E. Peter J.W. Rozenblit Department of Electrical and Computer Engineering University of Arizona Tucson Tucson AZ USA Department of Electrical Engineering and Computer Science University of California Irvine CA USA

this paper analyzes and compares the effectiveness of various system level design methodologies in assessing performance of embedded computing systems from the earliest stages of the design flow. the different methodologies are illustrated and evaluated by applying them to the design of an aircraft pressurization system (APS). the APS is mapped on a heterogeneous hardware/software platform consisting of two ASICs and a microcontroller. the results demonstrate the high impact of computer aided design (CAD) tools on design time and quality.

关键词： Embedded system Design engineering systems engineering and theory Design methodology Performance analysis System-level design Embedded computing Aircraft Hardware Microcontrollers

来源：评论

学校读者我要写书评

暂无评论

Fault tolerant data flow modeling using the generic modeling environment

Fault tolerant data flow modeling using the generic modeling...

引用

international conference and Workshop on Engineering of Computer-Based systems

作者： M.L. McKelvin J. Sprinkle C. Pinello A. Sangiovanni-Vincentelli Electrical Engineering and Computer Science Department University of California Berkeley CA USA General Motors Berkeley Laboratories Berkeley CA USA

Designing embedded software for safety-critical, real-time feedback control applications is a complex and error prone task. Fault tolerance is an important aspect of safety. In general, fault tolerance is achieved by duplicating hardware components, a solution that is often more expensive than needed. In applications such as automotive electronics, a subset of the functionalities has to be guaranteed while others are not crucial to the safety of the operation of the vehicle. In this case, we must make sure that this subset is operational under the potential faults of the architecture. A model of computation called fault-tolerant data flow (FTDF) was recently introduced to describe at the highest level of abstraction of the design the fault tolerance requirements on the functionality of the system. then, the problem of implementing the system efficiently on a platform consists of finding a mapping of the FTDF model on the components of the platform. A complete design flow for this kind of application requires a user-friendly graphical interface to capture the functionality of the systems with the FTDF model, algorithms for choosing an architecture optimally, (possibly automatic) code generation for the parts of the system to be implemented in software and verification tools. In this paper, we use the generic modeling environment (GME) developed at Vanderbilt University to design a graphical design capture system and to provide the infrastructure for automatic code generation. the design flow is embedded into the Metropolis environment developed at the University of California at Berkeley to provide the necessary verification and analysis framework.

关键词： Fault tolerance Application software Vehicle safety Computer architecture Fault tolerant systems Software design Embedded software Feedback control Error correction Hardware

来源：评论

学校读者我要写书评

暂无评论

9th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2003 Held as Part of the Joint European conferences on theory and Practice of Software, ETAPS 2003

9th International Conference on Tools and Algorithms for the...

引用

9th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2003 Held as Part of the Joint European conferences on theory and Practice of Software, ETAPS 2003

ISBN: (纸本)3540008985

the proceedings contain 44 papers. the special focus in this conference is on Bounded Model Checking, SAT-Based Methods, Mu-Calculus, Temporal Logics and Verification of Parameterized systems. the topics include: Automatic abstraction without counterexamples;experimental analysis of different techniques for bounded model checking;a generic on-the-fly solver for alternation-free Boolean equation systems;decidability of invariant validation for paramaterized systems;verification and improvement of the sliding window protocol;simple representative instantiations for multicast protocols;rapid parameterized model checking of snoopy cache coherence protocols;multiple-counterexample guided iterative abstraction refinement;verification of hybrid systems based on counterexample-guided abstraction refinement;counter-example guided predicate abstraction of hybrid systems;static guard analysis in timed automata verification;a tool for verifying timed automata and Estelle specifications;a new knowledge representation strategy for cryptographic protocol analysis;compositional analysis for verification of parameterized systems;learning assumptions for compositional verification;modular strategies for recursive game graphs;construction of efficient BDDS for bounded arithmetic constraints;modeling and analysis of power-aware systems;a set of performance and dependability analysis components for CADP;state class constructions for branching analysis of time Petri nets;using Petri net invariants in state space construction;optimistic synchronization-based state-space reduction;checking properties of heap-manipulating procedures with a constraint solver and an online proof-producing decision procedure for mixed-integer linear arithmetic.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Guest editors' introduction: Advancements and extensions of verification techniques

引用

international Journal on Software tools for Technology Transfer 2004年第2期6卷 99-101页

作者： Katoen, Joost-Pieter Stevens, Perdita Mathematics and Computer Science Formal Methods and Tools Group University of Twente 217 7500 AE Enschede Netherlands School of Informatics JCMB University of Edinburgh King's Buildings Mayfield Road Edinburgh EH9 3JZ United Kingdom

this special section is devoted to a selection of journal versions of papers that appeared originally in the Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS), which took place in Grenoble, France in April 2002 as a constituent event of the European joint conferences on theory and Practice of Software (ETAPS). All papers are relevant to the field of systems validation. the first three papers advance and extend model-checking techniques, the fourth presents algorithms for run-time verification, and the last paper is about animation and test generation for formal system specifications. © 2004 Springer-Verlag.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

tools and algorithms for the construction andanalysis of systems: 10th international conference, TACAS 2004 Held as Part of the Joint European conferences on theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - April 2, 2004 Proceedings 10th

Tools and Algorithms for the Construction andAnalysis of Sys...

引用

10th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2004 Held as Part of the Joint European conferences on theory and Practice of Software, ETAPS 2004

作者： Jensen, Kurt Podelski, Andreas University of Aarhus Department of Computer Science IT-parken Aabogade 34 Århus N Denmark Max-Planck-Institut für Informatik Stuhlsatzenhausweg 85 Saarbrücken Germany

来源：评论

学校读者我要写书评

暂无评论

Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic

Automatic parametric verification of a root contention proto...

引用

10th international conference on tools and algorithms for the construction and analysis of systems

作者： Beauquier, D Crolard, T Prokofieva, E Univ Paris 12 Lab Algorithm Complex & Log Val Marne France

ISBN: (纸本)354021299X

the paper presents a verification of the IEEE Root Contention Protocol as an illustration of a new and innovative approach for the verification of real-time distributed systems. systems are modeled with basic Gurevich abstract state machines (ASMs), and requirements are expressed in a first order timed logic (FOTL). FOTL is undecidable, however the protocol we study is in a decidable class of practical interest. Advantages of this framework are twofold: on the one hand, a great expressive power which permits in particular an easy treatment of parameters, on the other hand the modeling task is simplified by an adequat choice of tools.

关键词： parametric verification real-time distributed systems predicate logic IEEE 1394a standard root contention protocol Gurevich abstract state machines

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the 12th international conference on Nuclear Engineering (ICONE12) - 2004 Volume 1: Materials and Chemistry Issues;Next Generation systems;Student Paper Competition

Proceedings of the 12th International Conference on Nuclear ...

引用

12th international conference on Nuclear Engineering (ICONE12) - 2004

the proceedings contain 108 papers from Proceedings of the 12th international conference on Nuclear Engineering (ICONE12) 2004 Volume 1: Materials and Chemistry Issues Next Generation systems Student Paper Competition. the topics discussed include: steam generator analysis tools and modeling of degradation mechanisms;a technique for dynamic corrosion testing in supercritical CO2;use of Markov piping reliability models to evaluate time dependent frequencies of loss of coolant accidents;OECD pipe failure data exchange project (OPDE) and protective insulating coating for IGSCC mitigation in BWRs.

关键词： Nuclear reactors

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：