检索结果-南通市图书馆

Deadlock Detection in FPGA Design: A Practical Approach

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Tsinghua Science and Technology 2015年第2期20卷 212-218页

作者： Dexi Wang Fei He Yangdong Deng Chao Su Ming Gu jiaguang sun the Institute of Software Theory and Systems School of Software Tsinghua University

Formal verification of VHSIC Hardware Description Language （VHDL） in Field-Programmable Gate Array （FPGA） design has been discussed for many years. In this paper we provide a practical approach to do so. We present a semi-automatic way to verify FPGA VHDL software deadlocks, especially those that reside in automata. A domain is defined to represent the VHDL modules that will be verified; these modules will be transformed into Verilog models and be verified by SMV tools. By analyzing the verification results of SMV, deadlocks can be found; after looking back to the VHDL code, the deadlocking code is located and the problem is solved. VHDL verification is particularly important in safety-critical software. As an example, our solution is applied to a Multifunction Vehicle Bus Controller （MVBC） system for a train. The safety properties were tested well in the development stage, but experienced a breakdown during the long-term software testing stage, which was mainly caused by deadlocks in the VHDL software. In this special case, we managed to locate the VHDL deadlocks and solve the problem by the FPGA deadlock detection approach provided in this paper, which demonstrates that our solution works well.

关键词： Field-Programmable Gate Array （FPGA） VHSIC Hardware Description Language （VHDL） verification deadlocks Multifunction Vehicle Bus Controller （MVBC）

Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant

在线全文

学校读者我要写书评

暂无评论

Tsinghua Science and Technology 2014年第2期19卷 211-222页

作者： Hui Kong Fei He Xiaoyu Song Ming Gu Hongyan Tan jiaguang sun the School of Software Tsinghua University the Department of ECE Portland State University the Institute of Acoustics Chinese Academy of Sciences

To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.

关键词： inductive invariant semi-algebraic dynamical system safety verification hybrid system nonlinearsystem

Scan BIST with biased scan test signals

在线全文

学校读者我要写书评

暂无评论

Science in China(Series F) 2008年第7期51卷 881-895页

作者： XIANG Dong CHEN MingJing sun jiaguang School of Software Tsinghua University Beijing 100084 China Deptartment of Computer Science and Engineering University of California San Diego La Jolla CA 92093 USA

The conventional test-per-scan built-in self-test （BIST） scheme needs a number of shift cycles followed by one capture cycle. Fault effects received by the scan flipflops are shifted out while shifting in the next test vector like scan testing. Unlike deterministic testing, it is unnecessary to apply a complete test vector to the scan chains. A new scan-based BIST scheme is proposed by properly controlling the test signals of the scan chains. Different biased random values are assigned to the test signals of scan flip-flops in separate scan chains. Capture cycles can be inserted at any clock cycle if necessary. A new testability estimation procedure according to the proposed testing scheme is presented. A greedy procedure is proposed to select a weight for each scan chain. Experimental results show that the proposed method can improve test effectiveness of scan-based BIST greatly, and most circuits can obtain complete fault coverage or very close to complete fault coverage.

关键词： random testability scan-based BIST test signal biased random testing

An octree-based proxy for collision detection in large-scale particle systems

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2013年第1期56卷 55-64页

作者： FAN WenShan WANG Bin PAUL Jean-Claude sun jiaguang School of Software Tsinghua University Beijing Aerospace Control Center Department of Computer Science and Technology Tsinghua University Key Laboratory for Information System Security Ministry of Education of China Tsinghua National Laboratory for Information Science and Technology Institut National de Recherche en Informatique et en Automatique(INRIA)

Particle systems are important building block for simulating vivid and detail-rich effects in virtual world.One of the most difficult aspects of particle systems has been detecting collisions between particles and mesh surface.Due to the huge computation,a variety of proxy-based approaches have been proposed recently to perform visually correct simulation.However,all either limit the complexity of the scene,fail to guarantee non-penetration,or are too slow for real-time use with many particles.In this paper,we propose a new octree-based proxy for colliding particles with meshes on the GPU.Our approach works by subdividing the scene mesh with an octree in which each leaf node associates with a representative normal corresponding to the normals of the triangles that intersect the node.We present a view-visible method,which is suitable for both closed and non-closed models,to label the empty leaf nodes adjacent to nonempty ones with appropriate back/front property,allowing particles to collide with both sides of the scene mesh.We show how collisions can be performed robustly on this proxy structure in place of the original mesh,and describe an extension that allows for fast traversal of the octree structure on the GPU.The experiments show that the proposed method is fast enough for real-time performance with millions of particles interacting with complex scenes.

关键词： particle systems collision detection octree-based proxy GPU

The Modelling and Verification of PLC Program Based on Interactive Theorem Proving Tool COQ

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

The Modelling and Verification of PLC Program Based on Inter...

2011 International Conference on Computer Science and Information Technology(ICCSIT 2011)

作者： Litian Xiao Mengyuan Li Ming Gu jiaguang sun National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of EducationDepartment of Computer Science and Technology School of Software Tsinghua University Beijing Special Engineering Design and Research Institute National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of Education Department of Computer Science and Technology School of Software Tsinghua University

COQ is an interactive theorem proving tool. The paper abstractly describes the feature of COQ, the architecture and working modes of PLC program with the example of typical PLC. It also introduces the first-order logic syntax and semantics of Intuitionistic Logic. It briefly introduces the main Gallina language syntax elements, the corresponding use methods and main theorem proving tactic on COQ. The work has modeled kernel data type and basic statements and and the denotational semantics of PLC program with Gallina. It has given the correctness proof of PLC program based on theorem proving, i.e. based on semantics function the relationship of configuration between the before codes execution and the after is proved. The main purpose is to prove whether a PLC program satisfies certain nature within a scan period.

关键词： PLC Program Embedded System Verification Denotational Semantics Theorem Proving COQ

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

模糊测试中的静态插桩技术

计算机研究与发展 2023年第2期60卷 262-273页

作者：王明哲姜宇孙家广清华大学软件学院北京100084

模糊测试是一种行之有效的软件缺陷检测方法.其基本思想是生成大量随机输入,从而广泛探索程序行为,并以此发现程序崩溃和崩溃背后的软件缺陷.显然,纯随机的输入无法高效探索程序行为,大量程序缺陷也难以导致崩溃.为了进一步提升模糊测... 详细信息

模糊测试是一种行之有效的软件缺陷检测方法.其基本思想是生成大量随机输入,从而广泛探索程序行为,并以此发现程序崩溃和崩溃背后的软件缺陷.显然,纯随机的输入无法高效探索程序行为,大量程序缺陷也难以导致崩溃.为了进一步提升模糊测试的有效性,模糊测试往往引入静态插桩技术,用于加快探索程序状态空间速度,提升发现缺陷的能力.因此,引入静态插桩已经成为当下模糊测试的经典实践.聚焦于模糊测试场景下的插桩需求,除了介绍静态插桩技术的基本原理外,从安全特性强化和导向信息收集两个视角出发,系统性地分析了当下静态插桩的典型方法.同时,针对插桩的额外开销问题,全面地测量了不同插桩方案下的程序的执行速度,并与基线的未插桩程序进行比对.最后基于上述分析和测量,初步展望了静态插桩的优化方向.

关键词：静态插桩模糊测试软件缺陷程序分析额外开销

The Differential Equation Algorithm for General Deformed Swept Volumes

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2000年第6期15卷 604-610页

作者：汪国平华宣积孙家广 DepartmentofComputerScienceandTechnology PekinUniversityBeijing100871P.R.China

The differential equation approach for characterizing swept volume boundaries is extended to include objects experiencing deformation. For deformed swept volume, it is found that the structure and algorithm of sweep-envelope differential equation (SEDE) are similar between the deformed and the rigid swept volumes. The efficiency of SEDE approach for deformed swept volume is proved with an example.

关键词： CAD geometric modeling sweeping motion deformation swept volume

An Algorithm of B-Spline Surface Interpolation

在线全文

学校读者我要写书评

暂无评论

Computer Aided Drafting,Design and Manufacturing 1998年第2期8卷 38-42页

作者： Ning Tao Tang Rongxi sun jiaguang

A surface interpolation algorithm is presented. By using a special kind of knot vector. a B-spline surface can be constructed to interpolate an array of m ×n positions, including parameter u and v tangent vectors and twist vector at each positions. Single surface interpolation approach is easier to ensure the smoothness of the interpolating surface than multi-patches method. This algorithm can be used to solve the approximating problem of B-spline approximation of general parametric surface.

关键词： B-spline surface modeling twist vector

在线全文

学校读者我要写书评

暂无评论

关于《国家自然科学基金委员会章程》的说明

中国科学基金 2005年第3期19卷 136-138页

作者：孙家广国家自然科学基金委员会中国工程院院士副主任北京100085

2004年1月5日,国务委员陈至立同志在听取自然科学基金委工作汇报时指示"要做好国家自然科学基金委员会章程的制定工作".根据这一指示的要求,国家自然科学基金委员会(以下简称自然科学基金委)于2004年5月启动了(以下简称)的制定工作.制... 详细信息

2004年1月5日,国务委员陈至立同志在听取自然科学基金委工作汇报时指示"要做好国家自然科学基金委员会章程的制定工作".根据这一指示的要求,国家自然科学基金委员会(以下简称自然科学基金委)于2004年5月启动了(以下简称)的制定工作.制定的目的是深入贯彻党的十六届四中全会决定中提出的坚持"科学执政、民主执政、依法执政"的要求,确立国家自然科学基金委员会工作规范和行为准则,进一步推进科学基金科学管理、民主管理、依法管理的法制化进程,保障国家自然科学基金事业健康发展.

关键词：国家自然科学基金委员会章程 2004年1月 2004年5月制定工作工作汇报行为准则工作规范科学管理民主管理依法管理健康发展法制化贯彻