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

Program verification via iterated specialization

SCIENCE OF COMPUTER programming 2014年第Part2期95卷 149-175页

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G DAnnunzio DEC I-65127 Pescara Italy Univ Roma Tor Vergata DICII I-00133 Rome Italy CNR IASI I-00185 Rome Italy

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of imperative programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from any initial configuration. We introduce a CLP program I that encodes the interpreter of the language and defines a predicate unsafe equivalent to the negation of the safety property to be verified. Then, we specialize the CLP program I with respect to the given imperative program and the given initial and error configurations, with the objective of deriving a new CLP program I-sp that either contains the fact unsafe (and in this case the imperative program is proved unsafe) or contains no clauses with head unsafe (and in this case the imperative program is proved safe). If Isp enjoys neither of these properties, we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating information (either propagating forward from an initial configuration to an error configuration, or propagating backward from an error configuration to an initial configuration) and different operators (such as the widening and the convex hull operators) for generalizing predicate definitions. Each specialization step is guaranteed to terminate, but due to the undecidability of program safety, the iterated specialization process may not terminate. By an experimental evaluation carried out on a significant set of examples taken from the literature, we show that our method improves the precision of program verification with respect to state-of-the-art software model checkers. (C) 2014 Elsevier B.V. All rights reserved.

关键词： Software model checking constraint logic programming Program specialization Program transformation

来源：评论

学校读者我要写书评

暂无评论

Towards verification of computation orchestration

引用

FORMAL ASPECTS OF COMPUTING 2014年第4期26卷 729-759页

作者： Dong, Jin Song Liu, Yang Sun, Jun Zhang, Xian Natl Univ Singapore Sch Comp Singapore 117548 Singapore Nanyang Technol Univ Sch Comp Engn Singapore 639798 Singapore Singapore Univ Technol & Design Singapore Singapore

Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the operational semantics of Orc. Consequently, Timed Automata models are systematically constructed from Orc programs. The practical implication is that existing tool supports for Timed Automata, e.g., Uppaal, can be used to simulate and model check Orc programs. An experimental tool has been implemented to automate this approach. Secondly, we start with encoding the operational semantics of Orc language in constraint logic programming (CLP), which allows a systematic translation from Orc to CLP. Powerful constraint solvers like CLP are then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, lower or upper bound of a time interval, etc. Counterexamples are generated when properties are not satisfied. Furthermore, the stepwise execution traces can be automatically generated as the simulation steps. The two different approaches give an insight into the verification problem of Web Service orchestration. The Timed Automata approach has its merits in visualized simulation and efficient verification supported by the well developed tools. On the other hand, the CPL approach gives better expressiveness in both modeling and verification. The two approaches com

关键词： Orc Web service orchestration Verification Timed automata Uppaal constraint logic programming CLP(R)

来源：评论

学校读者我要写书评

暂无评论

Hybrid Solution Framework for Supply Chain Problems

Hybrid Solution Framework for Supply Chain Problems

引用

11th International Symposium on Distributed Computing and Artificial Intelligence (DCAI)

作者： Sitek, Pawel Wikarek, Jaroslaw Univ Technol Inst Management & Control Syst Kielce Poland

ISBN: (纸本)9783319075938;9783319075921

The paper presents application and implementation aspects of a hybrid approach to modeling and optimization for supply chain problems. Two environments of mathematical programming (MP) and constraint programming (CP) were integrated into Hybrid Solution Framework (HSF). The strengths of MP and CP, in which constraints are treated in a different way and different methods are implemented, were combined to use the strengths of both. The proposed approach is particularly important for the decision models in logistic and supply chain management, where an objective function and many discrete decision variables added up in multiple constraints.

关键词： constraint logic programming mathematical programming optimization supply chain management hybrid methods

来源：评论

学校读者我要写书评

暂无评论

Assertion-based Debugging of Higher-Order (C) LP Programs 14

Assertion-based Debugging of Higher-Order (C) LP Programs

引用

16th International Symposium on Principles and Practice of Declarative programming (PPDP)

作者： Stulova, Nataliia Morales, Jose F. Hermenegildo, Manuel V. IMDEA Software Inst Madrid Spain Tech Univ Madrid UPM Sch Comp Sci Madrid Spain

ISBN: (纸本)9781450329477

Higher-order constructs extend the expressiveness of firstorder (constraint) logic programming ((C) LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C) LP systems helping programmers detect errors and validate programs. However, these assertion-based extensions to (C) LP have not been integrated well with higher-order to date. This paper contributes to filling this gap by extending the assertion-based approach to error detection and program verification to the higher-order context within (C) LP. We propose an extension of properties and assertions as used in (C) LP in order to be able to fully describe arguments that are predicates. The extension makes the full power of the assertion language available when describing higher-order arguments. We provide syntax and semantics for (higher-order) properties and assertions, as well as for programs which contain such assertions, including the notions of error and partial correctness. We also discuss several alternatives for performing run-time checking of such programs.

关键词： logic programming constraint logic programming Program Verification Higher Order Run-time Verification Error Detection Debugging Assertions

来源：评论

学校读者我要写书评

暂无评论

A hybrid multi-agent approach to the solving supply chain problems 18th

A hybrid multi-agent approach to the solving supply chain pr...

引用

18th Annual International Conference on Knowledge-Based and Intelligent Information and Engineering Systems (KES)

作者： Sitek, Pawel Nielsen, Izabela Ewa Wikarek, Jaroslaw Kielce Univ Technol Inst Management & Control Syst PL-25314 Kielce Poland Univ Dept Mech & Mfg Engn Aalborg Denmark

The paper presents a concept and application of a hybrid multi-agent approach to modeling and optimization the supply chain problems. Two environments (mathematical programming (MP) and constraint logic programming (CLP)) and two types of agents were integrated. This integration and hybridization, complemented with an adequate transformation of the problem, facilitates a significant reduction of the combinatorial problem. The whole process takes place at the implementation layer, which makes it possible to use the structure of the problem being solved, implementation environments and the very data. The strengths of MP and CLP, in which constraints are treated in a different way and different methods are implemented, were combined to use the strengths of both. The proposed approach is particularly important for the decision models with an objective function and many discrete decision variables added up in multiple constraints. The presented multi-agent approach will be compared with classical mathematical programming on the same data sets and models. In addition, the proposed approach will be used for modelling and optimization of the hybrid model, which has not only linear constraints but also logical constraints. (C) 2014 The Authors. Published by Elsevier B.V.

关键词： multi-agent constraint logic programming mathematical programming optimization supply chain management hybridization

来源：评论

学校读者我要写书评

暂无评论

Evolution of Region Connection Calculus to VRCC-3D+

引用

NEW MATHEMATICS AND NATURAL COMPUTATION 2014年第2期10卷 103-141页

作者： Sabharwal, Chaman L. Leopold, Jennifer L. Missouri Univ S&T Comp Sci Dept Rolla MO 65409 USA

Qualitative spatial reasoning (QSR) is useful for deriving logical inferences when quantitative spatial information is not available. QSR theories have applications in areas such as geographic information systems, spatial databases, robotics, and cognitive sciences. The existing QSR theories have been applied primarily to 2D. The ability to perform QSR over a collection of 3D objects is desirable in many problem domains. Here we present the evolution (VRCC-3D+) of RCC-based QSR from 2D to both 3D (including occlusion support) and 4D (a temporal component). It is time consuming to construct large composition tables manually. We give a divideand- conquer algorithm to construct a comprehensive composition table from smaller constituent tables (which can be easily handcrafted). In addition to the logical consistency entailment checking that is required for such a system, clearly there is a need for a spatio-temporal component to account for spatial movements and path consistency (i.e. to consider only smooth transitions in spatial movements over time). Visually, these smooth movement phenomena are represented as a conceptual neighborhood graph. We believe that the methods presented herein to detect consistency, refine uncertainty, and enhance reasoning about 3D objects will provide useful guidelines for other studies in automated spatial reasoning.

关键词： Qualitative spatial reasoning region connection calculus composition smooth transition constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Model-based protocol log generation for testing a telecommunication test harness using CLP

Model-based protocol log generation for testing a telecommun...

引用

Design, Automation and Test in Europe Conference and Exhibition (DATE)

作者： Balck, Kenneth Grinchtein, Olga Pearson, Justin Ericsson AB Linkoping Sweden Ericsson AB Stockholm Sweden Uppsala Univ Dept Informat Technol Uppsala Sweden

ISBN: (纸本)9783981537024

Within telecommunications development it is vital to have frameworks and systems to replay complicated scenarios on equipment under test, often there are not enough available scenarios. In this paper we study the problem of testing a test harness, which replays scenarios and analyses protocol logs for the Public Warning System service, which is a part of the Long Term Evolution (LTE) 4G standard. Protocol logs are sequences of messages with timestamps;and are generated by different mobile network entities. In our case study we focus on user equipment protocol logs. In order to test the test harness we require that logs have both incorrect and correct behaviour. It is easy to collect logs from real system runs, but these logs do not show much variation in the behaviour of system under test. We present an approach where we use constraint logic programming (CLP) for both modelling and test generation, where each test case is a protocol log. In this case study, we uncovered previously unknown faults in the test harness.

关键词： 4G mobile communication Long Term Evolution logic programming protocols telecommunication computing telecommunication equipment testing CLP LTE 4G standard Long Term Evolution 4G standard constraint logic programming equipment-under-test message sequences mobile network entities model-based protocol log generation public warning system service system-under-test telecommunication development telecommunication test harness test generation timestamps user equipment protocol logs Alarm systems Computer architecture Long Term Evolution Mathematical model programming Protocols Testing

来源：评论

学校读者我要写书评

暂无评论

Program verification via iterated specialization

Program verification via iterated specialization

引用

Science of Computer programming

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. DEC University G. d'Annunzio Viale Pindaro 42 Pescara65127 Italy DICII University of Rome Tor Vergata Via del Politecnico 1 Roma00133 Italy CNR-IASI Viale Manzoni 30 Roma00185 Italy

关键词： Model checking Computer circuits Computer programming languages logic programming constraint logic programming Program specialization Program transformations Program Verification Software model checking

来源：评论

学校读者我要写书评

暂无评论

A Hybrid Multi-agent Approach to the Solving Supply Chain Problems

引用

Procedia Computer Science 2014年 35卷 1557-1566页

作者： Paweł Sitek Izabela Ewa Nielsen Jarosław Wikarek Kielce University of Technology Institute of Management and Control Systems 25-314 Kielce Poland University Department of Mechanical and Manufacturing Engineering Alborg Denmark

关键词： multi-agent constraint logic programming mathematical programming optimization supply chain management hybridization

来源：评论

学校读者我要写书评

暂无评论

Integrating answer set programming and constraint logic programming

引用

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE 2008年第1-4期53卷 251-287页

作者： Mellarkod, Veena S. Gelfond, Michael Zhang, Yuanlin Texas Tech Univ Lubbock TX 79409 USA

We introduce a knowledge representation language AC(C) extending the syntax and semantics of ASP and CR-Prolog, give some examples of its use, and present an algorithm, ACsolver, for computing answer sets of AC(C) programs. The algorithm does not require full grounding of a program and combines "classical" ASP solving methods with constraint logic programming techniques and CR-Prolog based abduction. The AC(C) based approach often allows to solve problems which are impossible to solve by more traditional ASP solving techniques. We believe that further investigation of the language and development of more efficient and reliable solvers for its programs can help to substantially expand the domain of applicability of the answer set programming paradigm.

关键词： Knowledge representation and reasoning Answer set programming constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：