检索结果-南通市图书馆

R-calculus without the cut rule

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2011年第12期54卷 2550-2563页

作者： LUO Jie & li wei state key laboratory of software development environment, school of computer science and engineering, beihang university, beijing 100191, china state key laboratory of software development environment School of Computer Science and Engineering Beihang University Beijing China

R-calculus is an inference system for deducing all possible changes when a theory is refuted by the facts. In this paper, we try to eliminate the cut rule in R-calculus by modifying the existing rules and by introducing new rules. The result is the R-calculus without the cut rule, which still preserves the reachability, soundness and completeness as R-calculus does. R-calculus without the cut rule is a formal inference system of logical connective symbols and quantifier symbols solely. It can serve as the theoretical foundation of the automation of revision calculus.

关键词： revision R-calculus cut rule

An algorithm to compute maximal contractions for Horn clauses

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2011年第2期54卷 244-257页

作者： LUO Jie & li wei state key laboratory of software development environment, school of computer science and Technology, beihang university, beijing 100191, china state key laboratory of software development environment School of Computer Science and Technology Beihang University Beijing China

In the theory of belief revision, the computation of all maximal subsets (maximal contractions) of a formula set with respect to a set of facts is one of the key problems. In this paper, we try to solve this problem by studying the algorithm to compute all maximal contractions for Horn clauses. First, we point out and prove the conversion relationship between minimal inconsistent subsets of union of the formula set and the set of facts and maximal contractions of the formula set with respect to the set of facts. Second, we prove a necessary condition of a set of Horn clauses to be minimal inconsistent. Then, based on these two conclusions, we propose an interactive algorithm to enumerate all minimal inconsistent subsets of a given set of Horn clauses and a second algorithm to compute maximal contractions from these minimal inconsistent subsets. Finally, we proposed an interactive algorithm to compute maximal contractions for Horn clauses by composing the above two algorithms.

关键词： maximal contraction minimal inconsistent set minimal subtraction Horn clause

A tetrahedral data model for unstructured data management

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2010年第8期53卷 1497-1510页

作者： li wei & LANG Bo state key laboratory of software development environment, beihang university, beijing 100191, china state key laboratory of software development environment Beihang University Beijing China

This paper proposes a tetrahedral data model for unstructured data management. The model defines the four components of unstructured data including: basic attributes, semantic characteristics, low-level features and raw data on its four facets, and the relations between these components. The internal implementation structure of the model and the data query language are designed and briefly introduced. This model provides a unified, integrated and associated description for different kinds of unstructured data, and supports intelligent data services such as associated retrieval and data mining. An example is given to demonstrate how to use the model for describing and manipulating data from a sample video base.

关键词： unstructured data data model query language associated retrieval intelligent services

Reliability-aware automatic composition approach for web services

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2012年第4期55卷 921-937页

作者： li Mu 1,2,li Bo 1,2 & HUAI JinPeng 1,2 1 state key laboratory of software development environment,beihang university,beijing 100191,china 2 school of computer science and engineering,beihang university,beijing 100191,china state key laboratory of software development environment Beihang University Beijing China school of computer science and engineering Beihang University Beijing China

In this paper,we study the reliability-aware synthesis problem for composing available services automatically and guaranteeing that the composed result satisfies the specification,such as temporal constraints of functionality and reliability,centered on a synthesis model for mediator of web services composition (CSM).This approach focuses on handling attributes and state relations,and permitting users and services to operate over them,i.e.,read /write their data values and compare them according to a dense state *** show that the reliability-aware synthesis problem for the specification is EXPTIME-complete and we give an exponential-time algorithm (CSM-NSA) which for a given formula ψ and a synthesis model,synthesizes available services in the library satisfying ψ over the synthesis model (if they exist) or responds with "not satisfiable" (otherwise).The specification ψ is a fragment of PCTL (probabilistic computation tree logic),obtained from "ordinary" CTL (computation tree logic) by replacing the EX,AX,EU and AU operation with their quantitative counterparts X >p,X =1,U >p,and U =1,*** opposed to NSA,we provide a more effective algorithm to replace the NSA algorithm called CSM-HSA (heuristic synthesis algorithm).Though HSA is an incomplete algorithm,the answer is *** experiments show that the HSA algorithm solves the problem of reliability-aware service synthesis effectively and efficiently.

关键词： reliability web services synthesis problem synthesis model heuristic algorithm

A formal semantics for program debugging

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2012年第1期55卷 133-148页

作者： li wei1&li Ning1,2 1state key laboratory of software development environment,school of computer science and engineering,beihang university,beijing 100191,china 2china Ship Research and development Academy,beijing 100192,china state key laboratory of software development environment School of Computer Science and Engineering Beihang University Beijing China china Ship Research and development Academy Beijing China

This work aims to build a semantic framework for automated debugging.A debugging process consists of tracing,locating,and fixing processes *** first two processes are accomplished by a tracing procedure and a locating procedure,*** tracing procedure reproduces the execution of the failed test case with well-designed data structures and saves necessary information for locating *** locating procedure will use the information obtained from the tracing procedure to locate ill-designed statements and to generate a system of fix-equations,whose solution will be used to fix the bugs.A structural operational semantics is given to define the functions of the tracing and locating *** of them are proved to *** main task of fixing process is to solve the *** turns out that for a given failed test case,there exist four types of fix-equations and three dierent solutions:1)The bug is solvable,i.e.,there exists a solution of the system of fix-equations,and the program can be repaired.2)There exists a structural design error in the program,i.e.,the system of fix-equations generated at each round of the locating procedure is solvable,but a new bug will arise when the old bug is being fixed.3)There exists a logical design error,and the system of fix-equations is not solvable.

关键词： debugging operational semantics failed test case fix-equations

A heuristic algorithm for cube packing with time schedule

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2010年第1期53卷 18-29页

作者： li wei1, HUANG WenQi2, JIANG DongChen1 & liU XiangLong1 1state key laboratory of software development environment, beihang university, beijing 100191, china 2school of computer science and Technology, Huazhong university of science and Technology, Wuhan 430074, china state key laboratory of software development environment Beihang University Beijing China school of computer science and Technology Huazhong University of Science and Technology Wuhan China

Packing problem has been proved to be an NP-hard problem. Many algorithms such as simulation annealing algorithm, genetic algorithm and other heuristic algorithms have been proposed to solve twodimensional and three-dimensional packing problem. To solve the cube packing problem with time schedule, this paper first introduces some concepts such as packing level, space distance and average neighbor birth order and then proposes a greedy algorithm. The algorithm tries every feasible corner greedily to calculate the space utilization, packing level, space distance, average neighbor birth order of this placement, and chooses the best placement according to these criteria. Theoretical analysis indicates that the time complexity of this algorithm is O(A2B2C2T 2n5). The experiments show that the average space utilization of non-guillotine cutting test cases is 98.81%, and the average space utilization of guillotine cutting test cases achieves 99.87%. Furthermore, optimal solutions of more than half cases are achieved by this algorithm. The experimental results show that this algorithm can solve the problem of cube packing with time schedule effectively and effciently.

关键词： cube packing problem time schedule packing level space distance average neighbor birth order

Optimized statistical analysis of software trustworthiness attributes

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2012年第11期55卷 2508-2520页

作者： ZHANG Xiao1,li wei2,ZHENG ZhiMing1,2 & GUO BingHui1 1key laboratory of Mathematics,Informatics and Behavioral Semantics,Ministry of Education,beihang university,beijing 100191,china 2state key laboratory of software development environment,beihang university,beijing 100191,china key laboratory of Mathematics Informatics and Behavioral Semantics Ministry of Education Beihang University Beijing China state key laboratory of software development environment Beihang University Beijing China

software trustworthiness has become one of the key restrictions for software service quality and the development of the software ***,trustworthiness attributes interlace structured and dynamical coupling relations,which causes great barriers for trustworthiness measurements of large-scale *** to the dynamical evolutionary characteristics of software trustworthiness attributes,this paper proposes a new approach for optimizing the trustworthiness measurement in terms the kernel trustworthiness attributes,and improves a downsize-optimized statistical analysis method for software trustworthiness attributes based on their nonlinear *** improved method considerably simplifies the trustworthiness assessment of largescale *** theoretical analysis and numerical simulations,the feasibility of this method is verified using two typical examples that illustrate the realization of the trustworthiness measurement.

关键词： software trustworthiness kernel attributes optimization statistical analysis

Complex conforming Delaunay triangulation

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2010年第6期53卷 1130-1140页

作者： MENG XianHai 1, li JiGang 1, YANG Qin 1, CAI Qiang 2 & CHEN QiMing 3 1 NLSDE, school of computer science and engineering, beihang university, beijing 100083, china 2 school of computer sciences, beijing Technology and Business university, beijing 100037, china 3 school of Mechanical engineering and Automation, beihang university, beijing 100083, china NLSDE School of Computer Science and Engineering BeiHang University Beijing China school of computer sciences Beijing Technology and Business University Beijing China school of Mechanical engineering and Automation BeiHang University Beijing China

A novel algorithm of conforming Delaunay triangulation for curved geometry is presented in the paper.A progress has been made for the problem puzzled Delaunay refinement where curved constraints cannot be accepted as input *** algorithm is based on a new sufficient condition for the existence of constraints in *** requires computing only the intersection between constraints and Voronoi edges or faces instead of the circum-sphere of curved *** the termination of the algorithm when small input angles exist in constraints, a weighted method is applied to ensure that the algorithm can terminate under any *** two-dimensional and three-dimensional results are also *** is shown that the algorithm has the capability of dealing with both linear and nonlinear constraints in a consistent way, without the need of maintaining triangular meshes on face constraints.

关键词： mesh generation Delaunay triangulation conforming curved constraints tetrahedralization weight

Content Addressable Storage Optimization for Desktop Virtualization Based Disaster Backup Storage System

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

china Communications 2012年第7期9卷 1-13页

作者： Ruan li Xiao lim in Zhu Mingfa state key laboratory of software development environment Beijing 100191 P. R. China school of computer science and engineering Beihang University Beijing 100191 P. R. China

This paper proposes a content addres sable storage optimization method, VDeskCAS, for desktop virtualization storage based disaster backup storage system. The method implements a blocklevel storage optimization, by employing the algorithms of chunking image file into blocks, the blockffmger calculation and the block dedup li cation. A File system in Use Space （FUSE） based storage process for VDeskCAS is also introduced which optimizes current direct storage to suit our content addressable storage. An interface level modification makes our system easy to extend. Experiments on virtual desktop image files and normal files verify the effectiveness of our method and above 60% storage volume decrease is a chieved for Red Hat Enterprise linux image files. key words： disaster backup; desktop virtualization; storage optimization; content addressable storage

关键词： disaster backup desktop virtualization storage optimization content addressable storage

维普期刊数据库