|
|
| LIFO > Team PRV : Parallelism virtual Reality and systems Verification |
|
research activities of the PRV team : Parallelism virtual Reality and system VerificationCurrent research applies our background in semantics, parallel processing and distributed systems to virtual reality, computer security and bioinformatics. Parallel computing and virtual realityAdvanced visualization systems coordinate several video projectors to constitute a large and high-resolution visual fiels displaying 3D stereo images in real time. They require costly parallel machines to attain real-time response. We propose an alternative approach with a PC cluster and standard graphic cards, but this raises parallelization and synchronization problems. We have thus developped an experimental software, NetJuggler based on the open software VRJuggler. We have also developped software components for swaplock, genlock and active stereoscopy. The swaplock component has necessitated hardware development jointly with LESI (IPO, Université d'Orléans). NetJuggler is distributed under GPL and integrated to Mandrake's Clic library. To this day our web site has received 3000 visits and is NetJuggler is used in universities to drive image caves such as the Futures Lab at Argonne, USA or the VRlab in Sweden. We work with BRGM on applying Virtual Reality to geographic information systems, with a Workbench installed in their Orléans premises and a new national RNTL project called GeoBench (coordinator BRMG, participants: LIFO, INRIA Grenoble, CEA and TGS Europe).
We have designed tools to write easily and validate parallel programs that match efficiently distributed-memory architectures. For example the BSML-Lib library expresses extensible algorithms with purely functional operations in CAML. We have developped optimisation algorithms for relational queries in databases; they are the only ones of their kind to be scalable to large parallel systems. These results have been adapted to GRID computing by the national ACI-GRID project CARAML, (coordinator LIFO, participants INRIA, University of Paris-7, University of Paris-12). A new project deals with the reconstruction of 3D objects from datapoint clouds from scanners. It is co-supervised with a member of LVR (ENSIB-Univ. Orléans) and a japanese researcher. Verification and computer securityWe propose several different approaches. i) An original tree grammar formalism, called TTSG (`Tree Tuple Synchronized Grammar') has been defined; and by applying this formalism to Unification problems and Rewrite reachability we have obtained some interesting decidabilty results. These can be applied in analyzing the security properies of certain infinite sytems. ii) An equational approach has been developed for the study of `synchronous' process algebras; and a formalism based on strong - not weak - bisimualtion, applicable to the analysis of information flow between processes, has beeen deduced under this equational approach. iii) Inside a France-Quebec research network linking LIFO to IMAG, LORIA, the Ecole Polytechnique and UQAM in Montreal, we develop tools for the security analysis of software in a distributed environment, e-commerce, and cryptosystem analysis. The tools adopt a multi-paradigm philosophy: equational unification, communicating systems, semi-mecanizable induction...Two prototypes have already been developed, for formal verification of finite communicating processes and UML state diagrams. Software development
Ongoing Research Actions |