591 research outputs found
Generation of Test Data Structures Using Constraint Logic Programming
No full textThe goal of Bounded-Exhaustive Testing (BET) is the automatic generation of all the test cases satisfying a given invariant, within a given bound. When the input has a complex structure, the development of correct and efficient generators becomes a very challenging task. In this paper we use Constraint Logic Programming (CLP) to systematically develop generators of structurally complex test data. Similarly to filtering -based test generation, we follow a declarative approach which allows us to separate the issue of (i) defining the test structure and invariant, from that of (ii) generating admissible test input instances. This separation helps improve the correctness of the developed test case generators. However, in contrast with filtering approaches, we rely on a symbolic representation and we take advantage of efficient search strategies provided by CLP systems for generating test instances. Through some experiments on examples taken from the literature on BET, we show that CLP, by combining the use of constraints and recursion, allows one to write intuitive and easily understandable test generators. We also show that these generators can be much more efficient than those built using ad-hoc filtering-based test generation tools like Korat
Program Transformation for Development, Verification, and Synthesis of Software
No full textIn this paper we briefly describe the use of the program transformation methodology for the development of correct
and efficient programs. We will consider, in particular,
the case of the transformation and the development of constraint logic programs
Transformation techniques for constraint logic programs with applications to protocol verification
No full textThe contribution of this thesis consists in the extension of the techniques for the transformation of constraint logic programs and the development of methods for the application of these techniques to the proof of temporal properties of parameterized protocols. In particular, we first introduce a method for proving automatically the total correctness of an unfold/fold transformation by solving linear equations and inequations over the natural numbers. We also propose a transformation-based method for proving first order properties of constraint logic programs which manipulate finite lists of real or rational numbers. Then, we extend the standard folding transformation rule by introducing two variants of this rule. The first variant combines the folding rule with the clause splitting rule for obtaining a more powerful folding rule. The second variant is tailored to the elimination of the existential variables occurring in a clause. For the standard folding rule and its two variants we develop the corresponding algorithms for automating their application. Finally, we propose a program transformation framework for proving temporal properties of parameterized protocols. Using this framework we encode the protocols and the temporal properties we want to prove as logic programs, and then we use the unfold/fold transformation technique for proving whether or not the properties holds
Recommended from our members
Fantastic Architecture and the Building of Europe in Valerio Evangelisti's Eymerich Fiction
No full textConcomitant with the horizontal expansion of EU territory through physical and political enlargement is a genealogy narrative, which emphasizes the ostensible roots of Europeanness in classical antiquity and Christianity. In the face of this sanitized genealogy, which lies at the heart of the European constitutional project, a range of alternative and more inclusive narratives circulate in contemporary European popular fiction. This paper focuses on a series of fantasy novels by the Italian author Valerio Evangelisti, featuring Inquisitor Eymerich as hero-investigator. In his highly popular novels, Evangelisti seeks to uncover layers of shared historical memory untainted with post-Enlightenment rhetoric.
The central architectural tropes of Evangelisti’s imaginary world are those of a castle and a convent, epitomizing the temporal and sacral power in European history. Each isolated from its outside environment and built on layer upon layer of subterranean chambers and corridors, the castle and the convent conceal a past quite different from the one championed in the official European genealogy. Memories of pagan worship and Islamic or Judaic learning – banished from the official rhetoric – continue to thrive, dark and threatening, in the subterranean strata of Evangelisti’s European edifice. Evangelisti thus provides an incisive critique of the official European story of origin, which threatens to suppress any alternative visions of European history or unorthodox avenues for European identity formation
Generalization strategies for the verification of infinite state systems
No full textWe 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
Stochastically timed predicate-based communication primitives for autonomic computing
No full textPredicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the
evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a
stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension raises a number of non-trivial
design and formal semantics issues with different options as possible solutions at different levels of abstraction. We discuss four of these options. We provide formal semantics and an illustration of the use of the language modeling a variant of a bike sharing system, together with some preliminary analysis of the system performance
Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs
No full textIn the literature there are various papers which illustrate the relationship between the unfold/fold program transformation techniques and the proofs of program properties both in the case of logic programs and in the case of functional programs.In this paper we illustrate that relationship in the case of constraint logic programs. We build up on results already presented, i.e.,where we have considered logic programs with locally stratified negation. The constraint logic programming paradigm significantly extends the logic-programming paradigm by allowing some of the atoms to denote constraints in a suitably chosen constraint domain. By using those constraints it is often possible to get simple and direct formulations of problem solutions
Program transformation for development, verification, and synthesis of programs
No full textThis paper briefly describes the use of the program transformation methodology for the development of correct and efficient programs. In particular, we will refer to the case of constraint logic programs and, through some examples, we will show how by program transformation, one can improve, synthesize, and verify programs
On StocS: A Stochastic Extension of SCEL
No full textPredicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension allows for quantitative modelling and analysis of system behaviour (e.g. performance) but rises a number of non-trivial design and formal semantics issues with different options as possible solutions at different levels of abstraction
- …
