| Proposition | |
|
soumis en
|
2005 |
| Projet INRIA : Everest | Organisme étranger partenaire : KTH |
| Unité de recherche INRIA : Sophia Thème INRIA : |
Pays : Sweden |
|
|
|
|
| Nom, prénom | Huisman, Marieke | Gurov, Dilian |
| Grade/statut | CR 1 INRIA |
lecturer |
| Organisme d'appartenance (précisez le département et/ou le laboratoire) |
INRIA Sophia Antipolis Everest Project |
KTH-IMIT Laboratory of Electronics and Computer Systems |
| Adresse postale | 2004, route des Lucioles BP 93 06902 Sophia Antipolis |
P.O.Box Electrum 229 SE-164 40 Kista Sweden |
| URL | http://www-sop.inria.fr/everest/Marieke.Huisman | http://www.imit.kth.se/~dilian |
| Téléphone | +33 4 92 38 79 45 | +46 8 790 41 03 |
| Télécopie | +33 4 92 38 50 60 | +46 8 751 17 93 |
| Courriel | Marieke.Huisman@inria.fr | dilian@imit.kth.se |
La proposition en bref
| Mots-clés :compositional verification,
concurrency,
security, mobility, smart devices |
| Thématique de la
collaboration
(environ 10 lignes) : To support the secure dynamic loading of applications on portable devices (such as mobile phones, television set top boxes and smart cards) one needs formal verification techniques to show that the co-existence and collaboration of several applications on a single device does not affect the overall well-functioning of the system. These techniques need to be compositional and efficient: new (and unknown in advance) applications can be accepted dynamically on the device, provided their innocuity has been established. In earlier collaborations (resulting in several papers and a best paper award) we have successfully developed algorithmic techniques for compositional verification of control-flow properties for sequential programs. However, since new generation smart devices allow multi-threading, the next important challenge is to develop (or extend) automatic techniques to handle threads. In addition, we plan to extend our techniques to data-flow properties by incorporating finite data domains (or finite abstractions). This extension will also require a careful rethinking of properties that can be handled with our method. |
| Résultats attendus:
- An algorithmic compositional verification method to support
the secure
dynamic loading of multi-threaded applications for smart devices. (The French coordinator of the project will be on maternity
leave during
the first half of 2005. Therefore, our collaboration will mainly take
place
during the second half of 2005, and not all expected results will be
fully
established in 2005.) |
The Royal Institute of Technology (KTH) is the largest technical university in Sweden. Its Laboratory of Electronics and Computer Systems has 26 lecturers and researchers on its faculty. The main research themes of the laboratory are Peer-to-peer Computing, Computer Security, Agent Based Systems, System-on-chip Design and Wireless Computing.
Dilian Gurov obtained a Ph.D. degree in Computer Science from the University of Victoria, Canada, in March 1998, on the topic of verification of communicating systems with value passing. He then worked as a senior researcher at the Swedish Institute of Computer Science in Stockholm, Sweden, where he participated in a project ErlVer on verifying Erlang programs, and in the European IST project VerifiCard on verification of Java Card programs. In the latter, he actively collaborated with Marieke Huisman and Gilles Barthe from INRIA Sophia Antipolis. Since March 2002, Dilian is a lecturer at the Laboratory of Electronics and Computer Systems at KTH in Stockholm, where he continued his participation in VerifiCard until the project expiry at the end of 2003. He is currently working on algorithmic techniques for compositional verification of programs with recursion, as well as on state space exploration based verification of open systems.
Irem Aktug obtained a M.Sc. degree in Computer Science from METU Ankara, Turkey, in June 2003. Since August 2003 she is a Ph.D. student at KTH, supervised by Dilian Gurov. Irem is working on the project SEFROS on state space exploration based verification of open systems, funded by the Swedish Research Council.
2. Intérêt de la collaboration entre les équipes :
Our cooperation does not receive any financial support.
- Dans le cas où votre proposition serait retenue, vous parait-il probable d'obtenir de l'organisme étranger partenaire un soutien financier ? Montant envisagé ?
We do not expect to receive any further financial support from KTH.
2. Echanges
Préciser le nom des personnes impliquées et les
dates
prévisibles de leurs déplacements
| DEPLACEMENTS |
|
||
|
|
|
|
|
| Chercheurs confirmés | D. Gurov, October 2005 1 week |
M. Huisman December 2005 1 week |
2 |
| Post-doctorants | - | ||
| Doctorants | I. Aktug, November 2005 2 weeks |
1 | |
|
Total
|
2 | 1 | 3 |
Estimated costs per visit: 1500 euro
Total estimated costs: 4500 euro