React-plus. robust theories for emerging applications in concurrency theory: processes and logic used in emergent systems.

This project proposal, REACT PLUS, addresses the development and application of formal methods in real-life systems. It takes the challenging task of developing the underlying theory and machine-assisted tools for verifying concurrent systems specified in a formalism we have recently developed, the NTCC calculus. Our intended applications are concurrent systems from three emergent domains: Namely, Security, Biology and Multimedia Semantic Interaction. More precisely, our teams have developed a concurrent constraint (cc) formalism for reasoning about reactive systems under the auspices of COLCIENCIAS and the French National Institute for Research in Computer Science and Control (INRIa) via the projects REACT and FORCES. The formalism, the NTCC process calculus [NPV02], has attained a wide range of applications in emergent areas such as Security, Biology and Multimedia Semantic Interaction. We used NTCC to establish important properties of the encoded applications, e.g, security breaches [OV08a], biological malfunctions [GPRF07] and rhythmic coherence [RV04]. Nevertheless, NTCC does not provide for automatic or machine-assisted verification of system properties. We deal with large systems, thus this kind of verification is essential to our applications. This issue, however, has hitherto been far too little considered for constraint-based formalisms. automatic verification of reactive systems poses a fundamental challenge due to the state explosion problem; the number of states a system has is exponential in the number of concurrent processes. We therefore propose to rise to this challenge by identifying NTCC fragments amenable to automatic verification and developing techniques and tools to machine assist the verification of system properties in NTCC. We envisage two complementary approaches: (1) automaton-based symbolic techniques and (2) abstract interpretation. automaton-based representations of systems are often used for automatic verification [VW86]. We already showed the decidability of the verification problem for NTCC by using automaton representations of systems and systems' properties [V05]. These representations, however, have a nonelementary space complexity (i.e., the space complexity is worse than exponential). Our plan is to use a novel symbolic approach to ameliorate this state space problem. Our symbolic approach consists in using temporal constraints to compact the state space by using them as succinct representations of many potential transitions from a state. abstract interpretation [CC92] aim at the efficient extraction of representative information from system specifications. They provide the theoretical guarantees that allow deducing properties of programs by processing their associated approximation and type information. By using these techniques, we expect to provide suitable abstract semantics and domains to obtain compact representations of the behavior of NTCC processes. This may facilitate their automatic verification by reducing the state space. Broadly speaking, we shall provide NTCC with automatic verification and simulation techniques and user-friendly tools that can be used by practitioners in our intended applications areas: Security, Biology and Multimedia Semantic Interaction. More precisely, our purpose is to show that concurrent constraintbased techniques can offer important benefits, such as runnable specifications and system properties assurance, to systems modeling in real applications. We would like to demonstrate that practitioners in different areas could be able to take advantage of these benefits, without spending undue training time and effort, by supplying the NTCC calculus with coherent tools, such as efficient simulators and automatic verifiers. We will explore ways to seamlessly integrate these tools into existent development environments in real application areas. We also aim at contributing to the area of concurrent constraint programming by devising novel techniques and formalisms that will allow an integrated modeling, execution and verification environment, similar to those available for other concurrency formalisms. The present proposal is intended as the natural continuation of the international project REACT which was co-funded by COLCIENCIAS from 2007 until 2009. REaCT was a productive research collaboration with over 15 international publications, one BSc thesis, one PhD thesis, and three international workshops, and involving 4 PhD students, 3 BSc students and 3 Masters students. REaCT PLUS involves the same institutions that carried out REaCT: Namely, La Universidad Javeriana de Cali, Universidad del Valle, the French National Institute for Research in Computer Science and Control (INRIa), the CNRS Laboratory for Informatics LIX at Ecole Polyechnique de Paris, and the Institute for Research and Coordination acoustic/Music (IRCAM).