1,721,030 research outputs found
Automatic Verification of Timed Concurrent Constraint Programs
No full textThe language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent
Constraint Programming (cc) paradigm that allows us to specify concurrent systems where
timing is critical, for example reactive systems. Systems which may have an infinite number of
states can be specified in tccp. Model checking is a technique which is able to verify finite-state
systems with a huge number of states in an automatic way. In the last years several studies
have investigated how to extend model checking techniques to systems with an infinite number
of states. In this paper we propose an approach which exploits the computation model of
tccp. Constraint based computations allow us to define a methodology for applying a model
checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm
of model checking for LTL to a specific logic defined for the verification of tccp and to
the tccp Structure which we define in this work for modeling the program behavior. We
define a restriction on the time in order to get a finite model and then we develop some
illustrative examples. To the best of our knowledge this is the first approach that defines a
model checking methodology for tccp
A framework for monitored dynamic slicing of reaction systems
Full text linkReaction systems (RSs) are a computational framework inspired by biochemical mechanisms. A RS defines a finite set of reactions over a finite set of entities. Typically each reaction has a local scope, because it is concerned with a small set of entities, but complex models can involve a large number of reactions and entities, and their computation can manifest unforeseen emerging behaviours. When a deviation is detected, like the unexpected production of some entities, it is often difficult to establish its causes, e.g., which entities were directly responsible or if some reaction was misconceived. Slicing is a well-known technique for debugging, which can point out the program lines containing the faulty code. In this paper, we define the first dynamic slicer for RSs and show that it can help to detect the causes of erroneous behaviour and highlight the involved reactions for a closer inspection. To fully automate the debugging process, we propose to distil monitors for starting the slicing whenever a violation from a safety specification is detected. We have integrated our slicer in BioResolve, written in Prolog which provides many useful features for the formal analysis of RSs. We define the slicing algorithm for basic RSs and then enhance it for dealing with quantitative extensions of RSs, where timed processes and linear processes can be represented. Our framework is shown at work on suitable biologically inspired RS models
Selected Papers of 11th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2002)
No full text
A Logic Programming Approach to Reaction Systems
Full text linkReaction systems (RS) are a computational framework inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RS have shown to be useful also for computer science applications, e.g. to model circuits or transition systems. Since their introduction about 10 years ago, RS matured into a fruitful and dynamically evolving research area. They have become a popular novel model of interactive computation. RS can be seen as a rewriting system interacting with the environment represented by the context. RS pose some problems of implementation, as it is a relatively recent computation model, and several extensions of the basic model have been designed. In this paper we present some preliminary work on how to implement this formalism in a logic programming language (Prolog). To the best of our knowledge this is the first approach to RS in logic programming. Our prototypical implementation does not aim to be highly performing, but has the advantage of being high level and easily modifiable. So it is suitable as a rapid prototyping tool for implementing several extensions of reaction systems in the literature as well as new ones. We also make a preliminary implementation of a kind of memoization mechanism for stopping potentially infinite and repetitive computations. Then we show how to implement in our interpreter an extension of RS for modeling a nondeterministic context and interaction between components of a (biological) system. We then present an extension of the interpreter for implementing the recently introduced networks of RS
Rule-based Verification of Web sites
No full textIn this paper, we develop a framework for the automated verification of Web sites, which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. First, we provide a rewriting-based, formal specification language which allows us to define syntac- tic as well as semantic properties of the Web site. Then, we formalize a verification technique which detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/missing Web pages inside the Web site. Useful information is gathered during the verification process which can be used to repair the Web site. Our methodology is based on a novel rewriting-based technique, called partial rewriting, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents. The framework has been implemented in the prototype GVerdi, which is publicly available
Nested Guarded Horn Clauses
No full textThis paper defines a new concurrent logic language, Nested Guarded Horn Clauses (NGHC). The main new feature of the language is its concept of guard. In fact, an NGHC clause has several layers of (standard) guards. This syntactic innovation allows the definition of a complete (i.e. always applicable) set of unfolding rules and therefore of an unfolding semantics which is equivalent, with respect to the success set, to the operational semantics. A fixpoint semantics is also defined in the classic logic programming style and is proved equivalent to the unfolding one. Since it is possible to embed Flat GHC into NGHC, our method can be used to give a fixpoint semantics to FGHC as well
Confluent semantic basis for the analysis of concurrent constraint logic programs
No full textThe standard operational semantics of concurrent constraint logic languages is not confluent in the sense that different schedulings of processes may result in different program behaviors. While implementations are free to choose specific scheduling policies, analyses should be correct for all implementations. Moreover, in the presence of parallelism, it is usually not possible to determine how processes will actually be scheduled. Efficient program analysis is therefore difficult as all process schedulings must be considered. To overcome this problem, we introduce a confluent semantics which closely approximates the standard (nonconfluent) semantics. This semantics provides a basis for efficient and accurate program analysis for these languages. To illustrate the usefulness of this approach, we sketch analyses based on abstract interpretations of the confluent semantics which determine if a program is suspension- and local suspension-free
- …
