Stages de la spécialité SAR: Use of formal methods to specify spatial-temporal constrains in outdoor computing


This stage takes place within a collaboration between Université P. & M. Curie and Rutgers University. This will be joint work with a student from each institution. Interaction over the Atlantic is expected ;-).

Rutgers University With more than 50,000 students, Rutgers, The State University of New Jersey, is one of the US major state university. Chartered in 1766, as Queens’ College, Rutgers is the eights institution of higher education to be founded in America before the IndependenceWar. The Department of Computer Science offers Bachelors’, Master and Ph.D. degrees in Computer Science, with emphasis in distributed systems, mobile networking, compilers, theoretical computer science, computer vision and bioinformatics. The Distributed Computing (Disco) Laboratory was created in 1998 to conduct research on network-centric computing, particularly in remote healing systems and outdoor distributed computing. Supported by National Science Foundation grants, Disco Lab groups ten Ph.D. students, several visiting students and a couple of undergraduate students each year, under the supervision of Liviu Iftode, Associate Professor of Computer Science at Rutgers and Head of the Disco Lab. More information about Disco Lab can be found at

Université P. & M. Curie (LIP6-SRC) Research of the SRC group focuses on systems made of interacting components. This includes :
- system design within the context of international standards such as the "Open Distributed Processing Reference Model" (RM-ODP)
- design and implementation of verification tools to increase reliability
- computer aided system deployment and implementation
- Design and implementation of reconfigurable platforms based on virtual machines
- design and implementation of enhanced services such as fault tolerance of migration

The SRC group actively participates in normalization committees such as OMG (Object management Group) or ISO. Numerous research centers are using the tools we developed for the verification of distributed application and algorithms by means of Petri Nets [3].


Monitoring and maintenance of computer systems is not only prohibitively expensive, but is unacceptably slow due to the complexity of software systems today. Even with a large and expensive workforce, human administrators cannot respond effectively to the monitoring and management requirements due to the speed of failure and attack propagation, the number of failure incidences, and the increasing sophistication of attacks on the infrastructure. The ultimate goal of our current research is to develop highly-effective self-defending computer systems that can perform automated monitoring, detection, diagnosis and repair actions on themselves or on other cooperating systems.

The basic block of the envisaged defensive architecture is the programmable backdoor [2, 3]. In our approach, a backdoor is a trusted piece of hardware or a software mechanism that can be programmed to execute defensive activities on the memory of a computer system, such as monitoring, identification and enforcement of invariants, and repairing when these invariants are violated. A backdoor can execute defensive tasks standalone or in cooperation with other backdoors [1]. The challenge is to express the properties to be monitored and the actions to be taken in a rigorous way in order to guarantee their effectiveness.

Work to be done

The objective of this stage is to evaluate the potential of using formal methods to define spatial programs to be executed in a physical world that continuously changes during the execution. The first step of this work is to constraint in the context of a case study : distributed object tracking executed as a cooperative task in a physical region. In a second phase, perspectives should be made in order to generalize the approach out of the studied case study. Main milestones of the work should be :

- 1. analyze the case study and extract the relevant information according to the spa- tial programming technique,
- 2. extract relevant properties to be preserved all over the execution,
- 3. formalize these into Petri nets [2],
- 4. verify these properties using the formal description,
- 5. check that the implementation technique, based on smart messages is consistent to the model and the properties that are verified,
- 6. evaluation of the model using the spatial programming simulator and implemen- tation over Smart Messages.

Based on the results, this work may continue as a PhD.

Mot-clé: SAR hors ATIAM, recherche

- Fabrice Kordon (UPMC) - 01 44 27 88 20 -
- Liviu Iftode (Rutgers) -



du 3/4/2006 au 30/9/2006

2768 euros


[1] Borcea C., Intanagonwiwat C., Kang P., Kremer U., and Iftode L. Spatial program- ming using smart messages : Design and implementation. In The 24th International Conference on Distributed Computing Systems (ICDCS 2004), 2004.

[2] C. Girault and R. Valk. Petri Nets for Systems Engineering. Springer Verlag, 2003.

[3] Iftode L., Borcea C., Kochut A., Intanagonwiwat C., and Kremer U. Programming computers embedded in the physical world. In The 9th IEEE Workshop on Future Trends of Distributed Computing Systems (FTDCS 2003), 2003.

[4] Iftode L., Borcea C., and Kang P. Cooperative computing in sensor networks. In The Handbook of Sensor Networks : Compact Wireless and Wired Sensing Systems, M. Ilyas (ed), CRC Press, 2004.

[5] LIP6-SRC. The Mars project homepage,, 2002.

[6] Kang P., Borcea C., Xu G., Saxena A., Kremer U., and Iftode L. Smart messages : A distributed computing platform for networks of embedded systems. In Special Issue on Mobile and Pervasive Computing, The Computer Journal, British Com- puter Society, 2004.

[7] Ni Y., Stere A., Kremer U., and Iftode L. Programming ad-hoc networks of mobile and resource-constrained devices. In The ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), 2005.

logo-spip E. Saint-James & F. Kordon - Master Informatique - UPMC Valid XHTML 1.0!
Calculé le 26 avril 2019 à 01h03min