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

Semantics of temporal constrained objects

JOURNAL OF logicAL AND ALGEBRAIC METHODS IN PROGRAMMING 2021年 119卷

作者： Kannimoola, Jinesh M. Jayaraman, Bharat Achuthan, Krishnashree Amrita Vishwa Vidyapeetham Dept Comp Sci & Applicat Amritapuri India Amrita Vishwa Vidyapeetham Amrita Ctr Cybersecur Syst & Networks Amritapuri India SUNY Buffalo Dept Comp Sci & Engn Buffalo NY USA

This paper presents the declarative and operational semantics for the paradigm of temporal constrained objects (TCOB). This modeling paradigm is an extension of basic constrained objects where objects specify the structure of a system and constraints specify its behavior. Temporal constrained objects have been shown to provide a clear and high-level declarative specification of the time-dependent behavior of complex dynamic systems. Two key features of this paradigm are series variables and metric temporal operators. The main contribution of this paper lies in showing how we can define the semantics of temporal constrained objects in terms of a new paradigm called temporal constraint logic programs (TCLP), which extend temporal logic programs with constraint-solving. Compared with the several other logical languages incorporating constraints and temporal logic, the TCLP paradigm offers a clear and direct way of translating temporal constrained object programs using three simple temporal predicates: first p, next p, and prey p. The key approach is to map each class in a TCOB program to a predicate in the TCLP paradigm. Thus, the semantics of recursively defined classes is expressed in terms of the semantics of recursively defined predicates, a well-understood topic. Given the close connections between TCLP and CLP, we take advantage of the semantics of CLP for providing the declarative and operational semantics of TCLP and thereby also of temporal constrained objects. (C) 2020 Elsevier Inc. All rights reserved.

关键词： Temporal constrained objects Series variables Metric temporal operators constraint logic programs Temporal constraint logic programs Semantics

来源：评论

学校读者我要写书评

暂无评论

Program Verification using constraint Handling Rules and Array constraint Generalizations

Program Verification using Constraint Handling Rules and Arr...

引用

Fundamenta Informaticae

作者： De Angelis, Emanuele Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio University of Chieti-Pescara Viale Pindaro 42 Pescara65127 Italy University of Rome Tor Vergata Via del Politecnico 1 Rome00133 Italy IASI-CNR Via dei Taurini 19 Rome00185 Italy

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

关键词： Integer programming Application programs Computer circuits Computer programming languages Encoding (symbols) logic programming Metadata Semantics constraint Handling Rules constraint logic Programming constraint logic programs Generalization operators Program transformations Program Verification Replacement strategy Transformation rules

来源：评论

学校读者我要写书评

暂无评论

A Rule-based Verification Strategy for Array Manipulating programs

A Rule-based Verification Strategy for Array Manipulating Pr...

引用

Fundamenta Informaticae

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using constraint logic programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple prog {φ} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

关键词： Integer programming Linear transformations logic programming Mathematical transformations Semantics constraint logic programs Imperative programs Integer constraints Partial correctness Program Verification Rule based verification Transformation rules Transformation systems

来源：评论

学校读者我要写书评

暂无评论

Generalization strategies for the verification of infinite state systems

引用

THEORY AND PRACTICE OF logic PROGRAMMING 2013年第02期13卷 175-199页

作者： Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio Senni, Valerio Univ G DAnnunzio Dipartimento Sci I-65127 Pescara Italy Univ Roma Tor Vergata Dipartimento Informat Sistemi & Prod I-00133 Rome Italy CNR Ist Anal Sistemi & Informat I-00185 Rome Italy LORIA INRIA F-54602 Villers Les Nancy France

We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.

关键词： computational tree logic constraint logic programs generalization strategies infinite state systems program specialization program verification

来源：评论

学校读者我要写书评

暂无评论

Generalization strategies for the verification of infinite state systems

Generalization strategies for the verification of infinite s...

引用

Theory and Practice of logic Programming

作者： Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio Senni, Valerio Dipartimento di Scienze Università 'G. d'Annunzio' Viale Pindaro 42 I-65127 Pescara Italy Dipartimento di Informatica Sistemi e Produzione Università di Roma Tor Vergata Via del Politecnico 1 I-00133 Rome Italy CNR-IASI Viale Manzoni 30 I-00185 Rome Italy LORIA-INRIA 615 rue du Jardin Botanique 54602 Villers-les-Nancy cedex France Dipartimento di Informatica Sistemi e Produzione Università di Roma Tor Vergata Via del Politecnico 1 I-00133 Rome Italy

关键词： logic programming Model checking Computational tree logic constraint logic programs generalization strategies Infinite state systems Program specialization Program Verification

来源：评论

学校读者我要写书评

暂无评论

On the verification of security-aware E-services

引用

JOURNAL OF SYMBOLIC COMPUTATION 2012年第9期47卷 1066-1088页

作者： Ranise, Silvio FBK Irst Trento Italy

Web services providing E-commerce capabilities to support business transactions over the Internet are more and more widespread. The development of such services involves several security issues ranging from authentication to the management of the access to shared resources according to a given business model. The capability of validating designs against fast evolving requirements is of paramount importance for the adaptation of business models to changing regulations and rapidly evolving market needs. So, techniques for the specification and automated analysis of web services to be used in security-sensitive applications are crucial in the development of these systems. In this paper, we propose an extension of the relational transducers introduced by Abiteboul, Vianu, Fordham, and Yesha for the specification of the transaction protocols of web services and their security properties. We investigate the decidability of relevant verification problems such as goal reachability (for the validation of use-case scenarios) and log validation (for detecting frauds) and provide sufficient conditions for their decidability. The extension we propose is two-fold. First, we add constraints to specify the algebraic structure of the resources manipulated by the transducers. Second, recursion is allowed (only) in policy rules to express important policy idioms such as delegation. Technically, decidability is obtained by a reduction to a decidable class of first-order formulae and fix-point computation to handle recursion. (C) 2012 Elsevier Ltd. All rights reserved.

关键词： Relational transducers Access control policies constraint logic programs Bernays-Shonfinkel-Ramsey class Model completeness

来源：评论

学校读者我要写书评

暂无评论

A backward analysis for constraint logic programs

引用

THEORY AND PRACTICE OF logic PROGRAMMING 2002年第4-5期2卷 517-547页

作者： King, A Lu, LJ Univ Kent Canterbury CT2 7NF Kent England Oakland Univ Rochester MI 48309 USA

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an ad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

关键词： abstract interpretation constraint logic programs backward analysis condensing groundness analysis

来源：评论

学校读者我要写书评

暂无评论

Transforming constraint logic programs

引用

THEORETICAL COMPUTER SCIENCE 1998年第1-2期206卷 81-125页

作者： Bensaou, N Guessarian, I Univ Paris 06 LITP F-75252 Paris France

We study "a la Tamaki-Sato" transformations of constraint logic programs. We give an operational and fixpoint semantics of our constraint logic programs;we extend the Tamaki-Sato transformation system into a transformation system for constraint programs including fold-unfold, substitution, thinning and fattening, and constraint simplifications;we give a direct proof of its correctness which is simpler than the Tamaki-Sato proof.

关键词： program transformations constraint logic programs least fixpoint semantics correctness

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：