Sites Inria

Version française

Partnership - International

Jean-Michel Prima - 22/10/2013

Franco-Indian Partnership on Formal Modeling

Researchers at Inria have developed a fruitful collaboration with two leading mathematical  institutes of southern India, a country where the decimal system, the concept of zero and the negative numbers were first conceptualized millennia ago. At the heart of current partnership lies the ambition of providing tools for formal modeling and verification of distributed systems. Among other things, progress in this field might help improve reliability of web services.

Chennai. Formely Madras. 6 million inhabitants. The throbbing economic engine of southeastern India. The second largest IT beehive on the subcontinent. And a major university hub boasting no less than two top-flight mathematical institutes: CMI and IMSc. In recent years, both entities have partnered with several research centers in France, including Inria in Rennes. This joint effort focuses on formal modeling and verification of distributed systems.
Noticeably enough, the story actually started in a third country. As French scientist Loïc Hélouët recalls, “we have had a collaboration with National University of Singapore (NUS) for several years and more specifically with professor P.S. Thiagarajan, a world renowned scientist who happens to be a native from India. It was through him that we were introduced to fellow Indian researchers in Chennaï.”  An academic quartet formed of NUS, CMI, IMSc and Inria was eventually settled in 2008.

Associated Team

The priviledged instrument of this collaboration has been a succession of three associated teams: CASDS, DST and the recently started DISTOL (1). “The crux of this new project is verification and supervision of distributed systems through formal modeling and automated reasoning on models. Our goal is to guarantee the correct functioning of a system. More often than not, programmers start writing code without building a model of the system that they develop. Our opinion is that this modeling effort is essential: it provides ways of thinking about correctness of a system before programming it, and hence to avoid bugs that are due to the system's design rather than to programming errors. Developping from scratch works fine... until the first major bug pops up.”  For vendors and editors, the consequence of such failures can swollen to nightmarish proportions, as bugs stemming from design errors are not easily discovered by simple code inspection, and can be hard to isolate. Furthermore, they may force a complete redesign of the whole system from the very beginning.

While the linchpin of this collaboration shifted to India, the driving theme also evolved significantly.  “Initially, we were focused on verification techniques for models representing telecommunication protocols. Then we started moving towards the realm of web services. Quite remarkably, we and our Indian colleagues came separately to the same realization. Whereas the big challenge of the previous decades consisted in verifying protocols, the world has embarked a new era where the question at stake is guaranteeing correctness of distributed applications on the web. That is actually a conclusion reached by a large part of our community.”

Compositional Architectures, calls for Formal Verification

Indeed, “running software on the vastness of the Internet raises a number of problems, such as issues related to scalability and heterogenity. A lot of applications running on the web use third party services, such as banking facilities. One might integrate a banking service in an application without fully understanding the nuts and bolts of that particular aspect. It is sub-contracted to someone else. As a result, we end up with an open system in which some parts are completely opaque, and viewed as interactions with the rest of the world.” But such compositional architectures call for a lot of formal verification, both to ensure that components interact well, but also that the overall assembled system is correct.

As Loïc Hélouët points out, model-based reasoning techniques are hardly a stapple in the industry yet. “These skills tend to remain within the walls of research laboratories, which is unfortunate. For there are great benefits to be gained from them. If one can muster enough time and energy to build formal models, it pays out!  Regrettably so far, nor we, nor our Indian counterparts have been able to find an industrial partner to whom we could transfer the experience that we have garnered in studying formal models. By the way, this is the very danger facing our community: we could well remain in our ivory tower until the end of times building research prototypes that would not eventually find any use in the real world. But there is no point in establishing difficult mathematical results if our models are built to no avail.” Which adds another item to the challenge list: convincing the industry that formal modeling helps building more robust systems, finding bugs more easily, and hence should be considered as an essential part of the development process.

Keywords: INRIA Rennes - Bretagne Atlantique