Reverse engineering interoperability by means of behavioural types.

Those that have expressed interest in this include researchers from at least the following institutions:

  • Aalborg University (Hans Hüttel)
  • University of Glasgow (Simon Gay)
  • University of Leicester (Emilio Tuosto)
  • University of Bologna (Mario Bravetti)
  • New University of Lisbon (António Ravaria)
  • University of Dortmund (Jakob Rehof)
  • University of Turin (Ugo de'Liguoro)

The challenge we see is that of “reverse engineering” interoperability in existing software systems.

One of the most controversial stories in Denmark over the past 10 years has been that of the IC4 trains. They were supposed to replace the IC3 trains from the early 1990s. The IC4 trains were ordered from the Italian company Ansaldo Breda but the whole project experienced a delay of several years. Moreover, the IC4 trains are useless, in large part due to buggy Italian software. The Danish state railways are stuck with IC4 trains and now have to analyze, debug and ultimately reverse engineer the software of the IC4 trains. Some of the software issues appear to have to do with communication within the components of the train.

When talking about session types we often have the top-down view that a complete system should be designed, with its communication structures and protocols and their specification as types, then implemented in a typed language; this is essentially the view of global types, projections and endpoints. It rather assumes that we design and control the complete system. A train is a closed system of this kind; however we have the same challenge in the setting of open systems. Systems-oriented people usually want to work in open environments; they want everything to be dynamic; they want and need to interface with systems that are outside the control of their designs. Moreover, in the setting of the Internet, systems are open by nature – services, servers and mobile devices come and go.

One way of trying to deal with these issues is to introduce dynamic checking, based on behavioural types, in order to guard the interfaces with external systems.

Another way would be that of type inference: if we can infer behavioural types / protocols for existing systems, then we can bring them into the controlled world, and design types for new components that will work with them. Many of the interesting properties in the settings described above are liveness properties – this is something that we are interested in in the setting of BETTY (cf. the most recent STSMs). Also, there is some work on algorithms in the setting of BETTY but far from as much as one would like. An important selling point is that type-based methods are algorithmically inexpensive.

Finally, one may also need to dynamically solve bugs (when monitoring the behaviour of components). One should not simply reject bad programs, but also (and specially!) correct them (automatically), in a provably sound way.

There are at least three kinds of related work.

Firstly, there is work on type inference for legacy software. George Necula et al. have a paper from 2002 on this. And Tobias Kuipers and Leon Moonen (formerly of CWI) have done important work on type inference for legacy code, in particular for COBOL; this involves translation from COBOL to an intermediate language. Moreover, the work appears to focus on large codebases, not on communicating systems.

Secondly, there the Anno Domini project from the late 1990s involving Jakob Rehof, Fritz Henglein and others. The challenge was to devise type inference strategies to existing software to prevent the notorious Year 2000 problem.

And finally, there is recent work on synthesizing protocols from binaries by Dawn Song and others. However, it does not seem to address this from the point of view of type inference.

A natural candidate for a protocol language would be a notion of behavioural types. This might involve both binary and multiparty session types. And it would be good to have notions of type systems that would work for more than one particular language.

As far as we can tell, this problem setting relates to some of the Horizon 2020 calls (the page numbers refer to the Horizon Annex describing the calls in LEIT (LEadership in Information Technology)):

  • Tools and Methods for Software Development (p. 23)
  • Internet of Things and Platforms for Connected Smart Objects (p. 67)
  • Cybersecurity, Trustworthy ICT (p. 71)

On the academic side this would be relevant for quite a few BETTY people. Here are some examples. Within the BETTY community we have work on algorithms (Imperial, ITU, Lisbon), work on general notions of type systems (several Italians, Aalborg, Uppsala) and work on formalizing proofs of correctness using proof assistants (Uppsala). As for industrial partners, it would make sense to have a smallish partner that could supply us with a case study and a larger partner that could benefit directly. We are currently in touch with two companies here.

 
horizonidea.txt · Last modified: 2014/01/27 19:02 by ugo.deliguoro
 
Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki