Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

grupos:avispa:react [2007/12/09 08:26]
japerez
grupos:avispa:react [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
 +====== REACT ======
 +** __Robust theories for Emerging Applications in Concurrency Theory__ **
  
 +A joint research effort between the [[http://avispa.puj.edu.co|AVISPA Research Group]] (Universidad Javeriana at Cali, Colombia), the Musical Representations Team at [[http://www.ircam.fr|IRCAM]] and the [[http://www.lix.polytechnique.fr/comete/|INRIA Team Comète]] (LIX, École Polytechnique de Paris, France). 
 +
 +REACT is supported by **COLCIENCIAS** (The Colombian Agency for Science and Technology Development).
 +
 +===== Motivation =====
 +**Concurrency theory** has made progress by extending well established
 +theories to capture new and wider phenomena. In particular, process
 +calculi such as CSP, CCS and the pi-calculus, originally designed to
 +reason about concurrent systems, have been extended or specialized to
 +cope with the advents of new technology. For instance, spi-calculus
 +extends the pi-calculus to reason about security; a phenomenon which
 +now pervades the informational world. More recently, the pi-calculus
 +has been tailored to model phenomena in biology, business process
 +modeling (workflow) and web services.
 +
 +**Process calculi** are used for modeling the above-mentioned phenomena
 +for at least two reasons. First, since these calculi have careful,
 +mathematical definitions, they can be used to provide careful and
 +high-level meaning to the applications specified using them. Second,
 +the theoreticians working on these calculi have developed rich
 +reasoning methods to reason about meaning and properties of
 +processes. From the application point-of-view, such reasoning methods
 +can be used to infer important properties about encoded applications.
 +
 +The above evidence suggests that for developing a theory of some
 +phenomena a research strategy is to see if it can arise as an
 +//extension// or specialization of an existing mature framework. This
 +strategy, at least with a little hindsight, is what lead us to a
 +research proposal on robust theories for complex emerging applications
 +areas of concurrency theory. Namely, 
 +  * Security Protocols, 
 +  * Biological Systems and 
 +  * Multimedia Semantic Interaction. 
 +Although these areas
 +differ significantly from one another, we shall argue that there is a
 +fundamental commonality in the nature of the analysis that one wants
 +to achieve in them.
 +
 +===== Approach =====
 +
 +**Concurrent Constraint Programming (CCP)** is a mature formalism which
 +combines the traditional operational view of process calculi with a
 +declarative one of processes based upon logic. This combination allows
 +CCP to benefit from the large body of techniques of both process
 +calculi and logic. Our teams have developed and implemented a
 +particular CCP timed process calculus which we called **NTCC**.
 +The calculus offers reasoning techniques such as a linear-temporal
 +specification logic and its corresponding proof system in which
 +reachability analysis can be elegantly carried out.
 +
 +Our teams have been using NTCC for analyzing security protocols,
 +biological phenomena and applications from multimedia semantic
 +interaction. **Reachability analysis** is central to all of them. In
 +security protocols if there is a way to reach a state where some
 +intruder knows your secret, then there is a secrecy breach. In
 +bacterial transcription, one ones to know if there is a gene
 +expression possible in a given gene regulatory network: this is a
 +reachability analysis problem. Multimedia Semantic Interaction
 +involve complex interactions in which we may wish to know that a
 +certain undesirable property will eventually arise; again a
 +reachability question.
 +
 +Despite the success of our applications of NTCC to the
 +above-mentioned areas, we have learned from our modeling experience
 +and theoretical studies that the NTCC calculus is not sufficiently
 +robust for them. For example, some security protocols use a mechanism
 +to allow generation and communication of secrets. The NTCC calculus
 +can at best express this mechanism indirectly. Also, the NTCC calculus
 +also lacks probabilistic techniques. The modeling of the biological
 +systems often requires to cope with uncertain and approximate
 +information, which one can refine by statistical measurements, and
 +which can then be naturally represented using a probabilistic
 +formalism. Furthermore, we have identified complex non-regular audio
 +processing temporal behaviour which cannot be expressed in NTCC.
 +
 +===== Goals and Expected Results =====
 +
 +Therefore, the main objectives of REACT focus on developing
 +more robust CCP theories for dealing with applications in the areas of
 +Security Protocols, Biology and Multimedia Semantic Interaction.
 +
 +We propose to obtain our objectives by tailoring the CCP process
 +calculus NTCC for each of these areas. We believe that our expertise
 +in process calculi and our experience in modeling these sort of
 +applications are fundamental for achieving this task.
 +
 +We expect both theoretical and practical results from our efforts on
 +this proposal. Namely: (i) CCP Process Calculi to model and reason
 +about phenomena in these areas. (ii) Tools to automatically simulate
 +and verify the encoded applications.
 
grupos/avispa/react.txt · Última modificación: 2011/01/24 15:30 (editor externo)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki