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

6th International Conference on Fundamental Approaches to Software Engineering, FASE 2003 Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2003

引用

6th International Conference on Fundamental Approaches to Software Engineering, FASE 2003 Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2003

ISBN: (纸本)3540008993

The proceedings contain 27 papers. The special focus in this conference is on Software components, Mobile computing, Aspect and object-oriented programming, Distributed and web applications, Software measurements, Formal verification, Analysis and testing and Model integrations and extensions. The topics include: An ontology for software component matching;a description language for composable components;a logical basis for the specification of reconfigurable component-based systems;an overall system design approach doing object-oriented modeling to code-generation for embedded electronic systems;composing specifications of event based applications;a Spatio-Temporal logic for the specification and refinement of mobile systems;spatial security policies for mobile agents in a sentient computing environment;towards UML-based formal specifications of component-based real-time software;modelling recursive calls with UML state diagrams;model-based development of web applications using graphical reaction rules;modular analysis of dataflow process networks;foundations of a weak measurement-theoretic approach to software measurement;an information-based view of representational coupling in object-oriented systems;a temporal approach to specification and verification of pointer data-structures;a program logic for handling java card’s transaction mechanism;automatic model driven animation of SCR specifications;probe mechanism for object-oriented software testing;integration of formal datatypes within state diagrams;towards a natural interoperability between XML and ER diagrams;detecting implied scenarios analyzing non-local branching choices and capturing overlapping, triggered, and preemptive collaborations using MSCs.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Checking properties of Heap-Manipulating procedures with a constraint solver

Checking properties of Heap-Manipulating procedures with a c...

引用

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

作者： Vaziri, Mandana Jackson, Daniel Laboratory for Computer Science Massachusetts Institute of Technology Cambridge MA United States

ISBN: (纸本)3540008985

A method for finding bugs in object-oriented code is presented. It is capable of checking complex user-defined structural properties - that is, of the configuration of objects on the heap - and generates counterexample traces with no false alarms. It requires no annotation beyond the specification to be checked, and is fully automatic. The method relies on a three-step translation: from code to a formula in a first-order relational logic, then to a propositional formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to find a solution that constitutes a counterexample. This underlying scheme, presented previously, does not scale readily. In this paper, we show how a suite of optimizations results in much improved scalability. The optimizations are based on a special treatment of relations that are known to be functional, and target all steps. The effect of the optimizations is demonstrated by application to the analysis of a red-black tree implementation. © Springer-Verlag Berlin Heidelberg 2003.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Correction of functional logic programs

引用

12th European Symposium on programming, ESOP 2003 Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2003

作者： Alpuente, Maria Ballis, Demis Correa, Francisco J. Falaschi, Moreno DSIC Universidad Politécnica de Valencia Camino de Vera s/n Apdo. 22012 Valencia46071 Spain Dip. Matematica e Informatica Via delle Scienze 206 Udine33100 Italy DIS U. EAFIT Cra. 49 N. 7 Sur 50 Medellín3300 Colombia

ISBN: (纸本)3540008861

We propose a new methodology for synthesizing correct functional logic programs. We aim to create an integrated development environment in which it is possible to debug a program and correct it automatically. We start from a declarative diagnoser that we have developed previously which allows us to identify wrong program rules w.r.t. an intended specification. Then a bug-correction, program synthesis methodology tries to correct the erroneous components of the wrong code. We propose a hybrid, top-down (unfolding–based) as well as bottom-up (induction–based), approach for the automatic correction of functional logic programs which is driven by a set of evidence examples which are automatically produced as an outcome by the diagnoser. The resulting program is proven to be correct and complete w.r.t. the considered example sets. Finally, we also provide a prototypical implementation which we use for an experimental evaluation of our system. © Springer-Verlag Berlin Heidelberg 2003.

关键词： Program debugging

来源：评论

学校读者我要写书评

暂无评论

Using controller-synthesis techniques to build property-enforcing layers

引用

12th European Symposium on programming, ESOP 2003 Held as Part of the Joint European Conferences on theory and practice of Software, ETAPS 2003

作者： Altisen, Karine Clodic, Aurèlie Maraninchi, Florence Rutten, Eric VERIMAG Centre Equation 2 Av. de Vignate GieresF38610 France LAAS-CNRS 7 av. Colonel Roche TOULOUSEF-31077 France INRIA Rhône-Alpes MONTBONNOT St Ismier CedexF-38334 France

ISBN: (纸本)3540008861

In complex systems, like robot plants, applications are built on top of a set of components, or devices. Each of them has particular individual constraints, and there are also logical constraints on their interactions, related to e.g., mechanical characteristics or access to shared resources. Managing these constraints may be separated from the application, and performed by an intermediate layer. We show how to build such property-enforcing layers, in a mixed imperative/ declarative style: 1) the constraints intrinsic to one component are modeled by an automaton;the product of these automata is a first approximation of the set of constraints that should be respected;2) the constraints that involve several components are expressed as temporal logic properties of this product;3) we use general controller synthesis techniques and tools in order to combine the set of communicating parallel automata with the global constraint. © Springer-Verlag Berlin Heidelberg 2003.

关键词： Automata theory

来源：评论

学校读者我要写书评

暂无评论

Model checking for probability and time: from theory to practice

Model checking for probability and time: from theory to prac...

引用

Annual Symposium on logic in Computer Science

作者： M. Kwiatkowska School of Computer Science University of Binningham Birmingham UK

Probability features increasingly often in software and hardware systems: it is used in distributed coordination and routing problems, to model fault-tolerances and performance, and to provide adaptive resource management strategies. Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic specifications such as "leader election is eventually resolved with probability 1", "the chance of shutdown occurring is at most 0.01%", and "the probability that a message will be delivered within 30ms is at least 0.75". A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. In contrast to conventional model checkers, which rely on reachability analysis of the underlying transition system graph, probabilistic model checking additionally involves numerical solutions of linear equations and linear programming problems. This paper reports our experience with implementing PRISM (***//spl sim/dxp/prism), a probabilistic symbolic model checker, demonstrates its usefulness in analyzing real-world probabilistic protocols, and outlines future challenges for this research direction.

关键词： Software performance Software systems Hardware Routing Fault tolerant systems Resource management Nominations and elections Probability Probabilistic logic logic programming

来源：评论

学校读者我要写书评

暂无评论

Disjunctive logic programs with inheritance

引用

theory and practice of logic programming 2002年第3期2卷 293-321页

作者： Buccafurri, F Faber, W Leone, N Univ Reggio Calabria DIMET I-89100 Reggio Di Calabria Italy Vienna Univ Technol Inst Informat Syst A-1040 Vienna Austria Univ Calabria Dipartmento Matemat I-87030 Arcavacata Di Rende CS Italy

The paper proposes a new knowledge representation language, called DLP<, which extends disjunctive logic programming (with strong negation) by inheritance. The addition of inheritance enhances the knowledge modeling features of the language providing a natural representation of default reasoning with exceptions. A declarative model-theoretic semantics of DLP< is provided, which is shown to generalize the Answer Set Semantics of disjunctive logic programs. The knowledge modeling features of the language are illustrated by encoding classical nonmonotonic problems in DLP<. The complexity of DLP< is analyzed, proving that inheritance does not cause any computational overhead, as reasoning in DLP< has exactly the same complexity as reasoning in disjunctive logic programming. This is confirmed by the existence of an efficient translation from DLP< to plain disjunctive logic programming. Using this translation, an advanced KR system supporting the DLP< language has been implemented on top of the DLV system and has subsequently been integrated into DLV.

关键词： nonmonotonic reasoning knowledge representation disjunctive logic programming inheritance exceptions

来源：评论

学校读者我要写书评

暂无评论

On properties of update sequences based on causal rejection

引用

theory and practice of logic programming 2002年第6期2卷 711-767页

作者： Eiter, T Fink, M Sabbatini, G Tompits, H Vienna Univ Technol Inst Informat Syst Abt Wissensbasierte Syst 184 3 A-1040 Vienna Austria

In this paper, we consider an approach to update nonmonotonic knowledge bases represented as extended logic programs under the answer set semantics. In this approach, new information is incorporated into the current knowledge base subject to a causal rejection principle, which enforces that, in case of conflicts between rules, more recent rules are preferred and older rules are overridden. Such a rejection principle is also exploited in other approaches to update logic programs, notably in the method of dynamic logic programming, due to Alferes et al. One of the central issues of this paper is a thorough analysis of various properties of the current approach, in order to get a better understanding of the inherent causal rejection principle. For this purpose, we review postulates and principles for update and revision operators which have been proposed in the area of theory change and nonmonotonic reasoning. Moreover, some new properties for approaches to updating logic programs are considered as well. Like related update approaches, the current semantics does not incorporate a notion of minimality of change, so we consider refinements of the semantics in this direction. We also investigate the relationship of our approach to others in more detail. In particular, we show that the current approach is semantically equivalent to inheritance programs, which have been independently defined by Buccafurri et al., and that it coincides with certain classes of dynamic logic programs. In view of this analysis, most of our results about properties of the causal rejection principle apply to each of these approaches as well. Finally, we also deal with computational issues. Besides a discussion on the computational complexity of our approach, we outline how the update semantics and its refinements can be directly implemented on top of existing logic programming systems. In the present case, we implemented the update approach using the logic programming system DLV.

关键词： logic programming knowledge-based updates nonmonotonic reasoning

来源：评论

学校读者我要写书评

暂无评论

Using methods of declarative logic programming for intelligent information agents

引用

theory and practice of logic programming 2002年第6期2卷 645-709页

作者： Eiter, T Fink, M Sabbatini, G Tompits, H Vienna Univ Technol Inst Informat Syst Abt Wissensbasierte Syst 184 3 A-1040 Vienna Austria

At present, the search for specific information on the World Wide Web is faced with several problems, which arise on the one hand from the vast number of information sources available, and on the other hand, from their intrinsic heterogeneity, since standards are missing. A promising approach for solving the complex problems emerging in this context is the use of multi-agent systems of information agents, which cooperatively solve advanced information-retrieval problems. This requires advanced capabilities to address complex tasks, such as search and assessment of information sources, query planning, information merging and fusion, dealing with incomplete information, and handling of inconsistency. In this paper, our interest lies in the role which some methods from the field of declarative logic programming can play in the realization of reasoning capabilities for information agents. In particular, we are interested to see how they can be used, extended, and further developed for the specific needs of this application domain. We review some existing systems and current projects, which typically address information-integration problems. We then focus on declarative knowledge-representation methods, and review and evaluate approaches and methods from logic programming and nonmonotonic reasoning for information agents. We discuss advantages and drawbacks, and point out the possible extensions and open issues.

关键词： multi-agent systems logic programming information agents

来源：评论

学校读者我要写书评

暂无评论

logic program specialisation through partial deduction: Control issues

引用

theory and practice of logic programming 2002年第4-5期2卷 461-515页

作者： Leuschel, M Bruynooghe, M Univ Southampton Dept Elect & Comp Sci Highfield SO17 1BJ England Katholieke Univ Leuven Dept Comp Sci B-3001 Heverlee Belgium

Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known respectively as partial evaluation and partial deduction, is to exploit partial knowledge about the input. It is achieved through a well-automated application of parts of the Burstall-Darlington unfold/fold transformation framework. The main challenge in developing systems is to design automatic control that ensures correctness, efficiency, and termination. This survey and tutorial presents the main developments in controlling partial deduction over the past 10 years and analyses their respective merits and shortcomings. It ends with an assessment of current achievements and sketches some remaining research challenges.

关键词： program specialisation logic programming partial evaluation partial deduction

来源：评论

学校读者我要写书评

暂无评论

A refinement calculus for logic programs

引用

theory and practice of logic programming 2002年第4-5期2卷 425-460页

作者： Hayes, I Colvin, R Hemer, D Strooper, P Nickson, R Univ Queensland Sch Informat Technol & Elect Engn St Lucia Qld 4067 Australia Victoria Univ Wellington Sch Math & Comp Sci Wellington New Zealand

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

关键词： refinement calculus logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：