Does Presenting Your Results Simply Damage Your Early Career Development?

Over the last couple of days, I have been peeking at Nicole Immorlica's enjoyable live report from FOCS 2007. This comment on a post of hers, amongst others, really got me thinking.

There is another factor going on here, which is that younger people often feel the need to "impress" the audience (both those in and outside their area) with how difficult their result is. For better or for worse, this is to some extent essential for grad students hoping to get faculty jobs, and assistant profs looking ahead to their tenure letters.

Once someone gets tenure, they can decide (depending on their personality) whether to keep up this ruse, or whether to aim to present results as simply as possible.

I agree that there is a general tendency amongst researchers at an early stage of their career to show off the hardness of their results, both in in their talks and in their papers. (I, for one, would write all of my early papers differently now.) However, I am not at all convinced that this is essential to foster one's early career, as claimed by the commentator.

When it comes to talks, as in other job-related things, I tend to be a follower of Paul Halmos. (See this compilation of his thoughts that recently appeared in the Notices of the AMS.)

....the purpose of a public lecture is to inform, but to do so in a manner that makes it possible for the audience to absorb the information. An attractive presentation with no content is worthless, to be sure, but a lump of indigestible information is worth no more.…

Less is more, said the great architect Mies van der Rohe, and if all lecturers remember that adage, all audiences would be both wiser and happier.

Have you ever disliked a lecture because it was too elementary? I am sure that there are people who would answer yes to that question, but not many. Every time I have asked the question, the person who answered said no, and then looked a little surprised at hearing the answer. A public lecture should be simple and elementary; it should not be complicated and technical.

I like to think that this is the message we should pass on to young researchers from the very beginning of their research careers. Building a reputation as a clear speaker, who can make difficult ideas and results accessible to her/his audience, can only help in one's career.

Isn't it going to be a huge bonus to be remembered as a person who gave a highly accessible and entertaining talk at FOCS/ICALP/LICS/SODA/STOC 2nnn? Why don't we tell our young colleagues that a talk at a generalist conference is essentially a public lecture? The result would be better talks at conferences, a happier audience, and an increased reputation for the speakers.

Call For Nominations: EATCS Award

The call for nominations for the EATCS Award 2008 has been published (pdf). The EATCS Award committee consists of Catuscia Palamidessi, David Peleg (chair), and Emo Welzl. Nominations should be sent to David Peleg by December 1, 2007. Further details on the award, including the stellar list of previous awardees, is here.

Be sure to nominate your favourite TCS researcher! The award will be delivered at ICALP'08 in Reykjavík.

Call For Nominations For The Gödel Prize 2008

The 2008 Gödel Prize for outstanding journal articles in the area of theoretical computer science, co-sponsored by EATCS and ACM SIGACT, will be awarded at ICALP 2008, which I am co-organizing in Reykjavík with Magnús M. Halldórsson and Anna Ingolfsdottir . The call for nominations, with deadline 31 January 2008, is now available here.

Make sure that you nominate your favourite paper in TCS for the award! One of the authors of the award-winning paper will attend the conference and will deliver a talk.

Deadline Approaching: Call for Workshops for ICALP 2008

The deadline for workshop proposals for ICALP 2008 is 31 October 2007. See the call for workshops for details on how to submit a proposal.

NordSec 2007

Over the last couple of days, ICE-TCS and the School of Computer Science at Reykjavík University hosted NordSec 2007, the 12th Nordic Workshop on Secure IT-systems. The workshop featured invited talks by Cedric Fournet (Microsoft Research, Cambridge, UK) and Greg Morissett (Harvard University, USA). I attended a few talks at the workshop (in between visits to my office to take care of typical daily chores and make sure that my inbox did not overflow), and chaired a session with short presentations.

I found the event interesting and enjoyable. In particular, the two invited talks were excellent. Cedric Fournet presented some joint work with Andrew D. Gordon and Sergio Maffeis reported in the paper A Type Discipline for Authorization in Distributed Systems. In his talk, Cedric addressed the following two key questions.

1. How can we express good authorization policies?
2. How can we enforce good authorization policies?

Cedric's tenet in the talk was that logics are good languages for expressing policies, and that type systems can be used enforce good policies at compile time. He also showed the audience what can be guaranteed at compile time when parts of the system are compromised, and the role that "robust safety" (safety despite compromised principals) plays in reasoning about processes.

Greg Morissett delivered an inspiring talk on the Cyclone project. Cyclone is a safe dialect of C. It is designed so that pure Cyclone programs are not vulnerable to a wide class of bugs that plague C programs such as buffer overflows. (Greg said early on in his talk that the legacy of C is, if you allow me to phrase one of his slides as a regular expression, (Buffer overrun)* and that he hates C!) Greg's talk was a great ad for some of the topics I am about to cover in my course on semantics for programming languages, and highlighted how good time-honoured theory in new clothes can help improve on the safety of a beast like C.

I think that his talk gave each member of the audience something to take home, and that's one of the main secrets of a successful invited address. I just wish that more of my colleagues had been there to listen.

CONCUR 2009

Breaking news! I am pleased to announce that CONCUR 2009 will be held in Bologna, and will organized by Mario Bravetti and Gianluigi Zavattaro. This will be the second Italian CONCUR after Pisa 1996.

Congratulations to Bologna, which hosts one of the strongest CS departments in Italy and is a hotbed of concurrency-theoretic research, and to CONCUR for visiting a lovely city.

Prize Time

It is the time of the year when prize announcements are out fast and furious.

The ink has not yet dried on the news announcing that the 2007 Nobel prize for medicine has been awarded to Mario R. Capecchi, Sir Martin J. Evans and Oliver Smithies "for their discoveries of principles for introducing specific gene modifications in mice by the use of embryonic stem cells". (I notice that Mario Capecchi is yet another Italian expatriate who, like Fermi and Segre before him, has become a US citizen.)

In mathematics/CS, László Lovász has received the Bolyai Prize, and Ben Green, Hershel Smith Professor of Mathematics at Cambridge University (UK), will receive the 2007 SASTRA Ramanujan Prize "for his phenomenal contributions to number theory by himself and in collaboration with Terence Tao, that have changed the face of combinatorial additive number theory."

Tomorrow is the turn of the Nobel prize for physics. It'll be interesting to see who receives it. I hope for an award to an Italian in Italy :-)

Frits Vaandrager's Answers

I have received a contribution from Frits Vaandrager to the discussion arising from the CONCUR workshop. I am very pleased to post them here.
Enjoy!

# What is the role/importance of real-time in modelling? Does industry want dense-time or discrete-time models?

When modelling embedded systems and/or protocols, real-time aspects have to be dealt with very frequently. If one prefers not to use a real-time model checker, one can often encode
real-time constraints in finite state model checkers. For instance, in an STTT paper from 2002, Brinksma, Mader and Fehnker analyzed a PLC control schedule using SPIN, and obtained results that were (at that time) competitive with Uppaal. Their trick was to advance the discrete clock variable not one by one, but directly to the point of the next event.

In his PhD thesis, Rajeev Alur has made a good case for dense time models. In the case of open systems with components that have different clocks, dense time is conceptually the right
thing to do. But in practice one often gets away with discrete-time models.

Industry has no preference for dense-time or discrete-time: any approach that solves their problems is fine.


# How does one involve small- and medium-size companies in collaborations with concurrency theoreticians/practitioners? Does "company size" matter?

The maturity of model checkers has increased enormously over the last years and as a result it becomes much easier to apply them, also for non-experts. I give two examples:

- Allen B. Downey has written "The little book of semaphores", a nice book in which he presents solutions to dozens of concurrency problems, ranging from classical ones (like the barbershop)
to tricky and obscure problems (like the Sushi bar). This year I asked a class of first-year computer science students with just a few hours of model checking experience to pick a problem from Downey's book (a different problem for each pair of students) and to model and analyze Downey's solution for it using Uppaal. As a result, my students spotted several mistakes in Downey's book, mistakes which have been confirmed by the author.

- Matthijs Mekking, a student interested in implementing protocols and with no particular expertise in formal methods just completed an MSc thesis project at NLnet Labs on the SHIM6
protocol, a proposed IETF standard for multi-homing. At some point he started to model the protocol using Uppaal and became enthusiastic. He managed to find several nontrivial mistakes
in the standard and greatly impressed the protocol designers. His results directly influenced the new version of the standard. (See http://www.ita.cs.ru.nl/publications/papers/fvaan/SHIM6/)

SMEs usually don't have verification specialists in house, so they need some advice on modelling and analysis. But with todays technology it is possible to get results rather quickly, and they can do part of the work themselves. The situation will further improve when MSc and PhD graduates with a background in model checking get jobs at these companies. My group is collaborating with several SMEs and the verification problems they provide us with are often
interesting from an academic perspective.

Unlike SMEs large companies are able to invest in long-term research.

# Is there any need for stochastic and probabilistic modelling in applications? More pointedly, have you met an example that you could not model because your tool does not support stochastic or probabilistic phenomena?

Yes!! There is a great need for stochastic and probabilistic modelling and analysis techniques, and I would for instance welcome a tool that combines the functionality of Uppaal and PRISM.

The Zeroconf protocol, for instance, is full of probabilistic features that we could not model using Uppaal. If we really want to make impact in the area of wireless sensor networks, mobile ad-hoc networks, and P2P networks we need to extend model checkers with probabilities since the design of these networks can only be properly understood if we take probabilities into account.

# How can we, as a community, foster the building of industrial-strength tools based on sound theories?

Theory for the sake of theory is good and important but IMHO the concurrency community has too much of it. In order to really push model checking technology into industry the performance and functionality of these tools must be further improved by several orders of magnitude. This can only be achieved by a combined and focused effort of a large team of researchers and is also a major academic challenge.

In order to test new ideas one needs prototype tools to play with. However, I believe it is not healthy that almost every research group on model checking has its own tool. Only a few groups manage to keep their model checking tool in the air for more than a decade. Developing an
industrial-strength model checking tool requires a huge effort. I think academic groups have to join forces if they want to build (and maintain!) industrial-strength tools. Uppaal has been highly succesful in part due to the continued efforts from teams in Aalborg, Uppsala, Nijmegen, Twente and elsewhere. So why don't the CADP and muCRL teams join forces? Why isn't it possible to establish stronger ties between Uppaal and IF? Why are there so many probabilistic model
checkers?

By combining efforts we can be much more effective.

# What has concurrency theory offered industry so far? What are the next steps that the concurrency community should take in order to increase the impact of its research in an industrial setting? And what are future promising application areas for concurrency research?

Contributions are very powerful modeling languages and concepts, and of course model checking.

A major challenge ahead of us is to combine features. In model checking people proposed symmetry reduction, partial order reduction, CEGAR, etc. What about the combination of all these features? How can we prove it is sound. Can we combine probabilistic choice, hybrid aspects, real-time, and hierarchy as in state-charts? I believe it will be possible to define such combinations but I expect we will need theorem provers and proof assistents to help us to manage the resulting complexity.

I am aware of applications in other areas, but I believe computer system engineering will remain the most important application area for concurrency theory the coming decade.

Joost-Pieter Katoen On The Need for Probabilistic and Stochastic Modelling

I am posting this message on behalf of Joost-Pieter Katoen, who sent me his reaction to one of the questions posed to the panel members during our workshop at CONCUR 2007. Enjoy!

I'd like to answer to the question on the need for stochastic and probabilistic modeling (and analysis). Some concrete examples of case studies provided by industry for which probabilistic aspects are very important are listed below. The importance of explicitly modeling random effects explicitly stands or falls with the kind of property to be established, of course, so I am definitely not claiming that these examples cannot (and should not) be modeled by techniques that do not support random phenomena.

1. Leader election in IEEE 1394: in case of a conflict (two nodes
pretend to be a leader), the contending nodes send a message (be
my parent) and randomly wait either short or long. What is the
optimal policy to resolve the contention the fastest? (This turns
out to be a slightly unbiased coin).

2. In the Ametist EU-project, the German industrial partner Axxom
generated schedules for a lacquer production plant. While doing
so, they abstracted from many details that the lacquer producer
supplies such as: the average fraction of time a resource is not
operational, the fraction of (operational) time the resource can
be used because necessary human support is present, and so
forth. In their abstraction they scheduled tasks conservatively
and they were interested in whether they could improve their
schedules while reducing the probability to miss the deadline.
Clearly, a stochastic modeling is needed, and indeed has been
carried out using a stochastic process algebra.

3. Hubert and Holger should be able to say much more about
a recent project they are pursuing with a French company on
the validation of multiprocessor multi-threaded architectures.
I do not know exactly what they are investigating, but they use
stochastic process algebras to model!

Finally, let me say that (as Moshe is also indicating) that the
interest in probabilistic modeling is growing steadily. To give
an example, the European Space Agency (ESA) is currently
considering to use probabilistic modeling and analysis in the
context of AADL, an architecture specification language where
an important ingredient ais the failure rates of components.

All in all, it is fair to say that there is a quest for probabilistic
techniques!

Joost-Pieter Katoen

CNRS Bronze Medal To Concurrency Theorist

I learned last night that Patricia Bouyer (CNRS researcher at LSV, ENS Cachan) has received a CNRS bronze medal 2007 in section 7. The CNRS bronze medal is awarded for outstanding achievement by a junior researcher.

Congratulations to Patricia, with whom I was lucky enough to work on this paper. At that time, Patricia was a freshly minted MSc student, but her talent was already abundantly clear. I recall that we were trying to show that a property language was sufficiently expressive to describe all of the properties of timed automata that could be checked by reachability analysis in the context of a test process. Patricia constructed a test process which had no counterpart in the property language, and this led to a strengthening of the property language, which we eventually were able to prove expressively complete.

From those early days, Patricia has gone from strength to strength, as witnessed by her impressive output. I believe that there is much more to come from her.

Reverse Age Discrimination

Every now and then, I rant on this blog about Italian academia. I do this because of the strong ties I have with my country (or in typical Italian fashion I should say "well, actually, with my region Abruzzo" or even "with my home town, Pescara" :-)) , and because I am saddened by the frustration I sense in the Italian colleagues I meet at conferences or I exchange emails with.

The latest installment of the saga of Italian academia I read is the commentary Reverse Age Discrimination written for Nature Physics by Francesco Sylos Labini and Stefano Zapperi, two physicists based in Rome. Their piece paints a rather bleak picture for young Italian scientists and reports on what they call "Lo Tsnunami dell'Universita' Italiana" (The Tsunami of Italian University). I encourage you to read their opinions and to look at the statistics they report on here.

The figures are amazing. Italian universities have an unusually large fraction of old professors. In Italy, 41% of the university professors are aged 60 or older and only 4% are below 40. If we consider full professors only, we discover that overall in Italy more than 47% are aged 60 or older, but for physicists this percentage reaches a hefty 64%!

Add to this picture that Italian universities have a very irregular recruitment flow, with sudden bursts of hiring based on seniority rather than on merit, and you will see that the only option
left for several talented young scientists is to move to other countries. The commentary reports that this year the French National Research Council (CNRS) selected seven young researchers (CR2) in theoretical physics, out of whom four were Italians! If we look at CS, let me go on record once more as saying that Italians in Paris would form a very strong TCS department by any measure.

Let me close by quoting from the last paragraph in the article.

To conclude, we acknowledge that some older scientists are active and productive, and that European countries should do something to keep them engaged. .... The broad question of how to use the experience of older faculty without hindering the advancement of the younger generation remains an important challenge.

I hope that this is a challenge that Italy's academic establishment will face very soon. The future of Italian science depends on it.

Luca de Alfaro in the News

At CONCUR 2007, I learned that our colleague and member of WG1.8 Luca de Alfaro has recently hit the news for his work on an evaluation of trust in contributions to Wikipedia. (See Demo: Coloring the text of the Wikipedia according to its trust.) Luca's work is based on the idea of colouring the text of Wikipedia articles according to a computed value of trust. The trust value of each word of a Wikipedia article is computed as a function of the reputation of the original author, as well as the reputation of all authors who subsequently revised the text.

This work of Luca's was mentioned in the Washington Post (I cannot locate the link anymore), the Jerusalem Post, ACM TechNews and SFGate.com amongst others.

Luca will also be the PC chair for FOSSACS 2009 in York, but this will give him less media exposure :-)

Nadia Busi (1968-2007)

During the excursion for CONCUR 2007, while visiting the Arrábida Convent, we were hit by the sad news that our colleague and friend Nadia Busi had suddenly passed away the night before. A paper having Nadia as one of the authors had been presented at the conference just before we set off for the excursion.

Our community has lost a very active and creative researcher, a woman who could be an example for others to follow and, above all, a very kind human being.

An obituary for Nadia, written by Roberto Gorrieri, will appear in the October issue of the BEATCS. You can read it here.

"We are such stuff
As dreams are made on, and our little life
Is rounded with a sleep."
(Shakespeare, "The Tempest")

Guest Post from Jorge Perez

I received this contribution from Jorge Perez, and post it with pleasure.

I have found your reports on the WG1.8 Workshop extremely enlightening. I am specially impressed by the invited speaker's opinions on the role of probabilistic/stochastic modeling. In my opinion, and having little experience on the theoretical side of the topic, their positions are, at the very least, certainly a matter for debate.

The topic of the workshop also made me remember of the spirit of my former research group in Colombia. For many reasons, the group (called AVISPA, see http://avispa.puj.edu.co/) is interested essentially in applied concurrency. This means thinking at the same time in theory and usable applications, beyond prototypes. Perhaps the most successful application area has been Computer Music.
In collaboration with the French Acoustics/Music Research Institute (IRCAM), AVISPA has designed and implemented formal, concurrent languages to assist music composers in their duties. I know this is not properly an 'industrial application' but it could be an example of how concurrency theory can be fruitfully applied.

AVISPA has recently launched a project on applied concurrency: it is
called REACT (see
http://cic.puj.edu.co/wiki/doku.php?id=grupos:avispa:react), and it aims at consolidating our concurrency languages in several application areas, including security, systems biology, computer music (or more generally: multimedia semantic interaction).

Sorry for the long post, but the topic is very interesting for me and I wanted to share this (perhaps unusual) approach to applied concurrency.

Some Answers By the Workshop Speakers

In a previous post, I listed the questions that the attendees at our CONCUR 2007 workshop raised to the invited speakers and panel members. I also promised to pen down my recollections of their answers. Here they, hoping that I won't misrepresent the opinions of these colleagues too much. I am sure that they will correct me if I inadvertently do so. Anything I write below should be taken with a huge pinch of salt :-)

What is the role/importance of real-time in modelling? Does industry want dense-time or discrete-time models?

Kim G. Larsen (KGL): The vast majority of computing systems in operation today are embedded. Proper modelling and analysis of the behaviour of embedded systems requires time. However, industry does not really seem to care whether the model of time used in the models is discrete or continuous. When analyzing embedded systems, quantitative analysis techniques are needed and I expect that stochastics will play an increasing role in the future.

Jan Friso Groote (JFG): Basically, industry do not know what they want and there is little point in chasing their ever-changing needs. Concrete modelling and analysis of computing systems should be based on a uniform calculus, which is rich enough to model the problem scenarios at hand. As far as real-time is concerned, it should be expressible in the uniform calculus.

How does one involve small- and medium-size companies in collaborations with concurrency theoreticians/practitioners? Does "company size" matter?

Both JFG and KGL reported on several examples of interaction with industry where there seemed no relation between "size" and the success of the interaction. Kim described a successful collaboration on testing of GUI applications with a one-person company having basically no technological expertise. This was compared with the collaboration with Bang and Olufsen, which was a failure despite the resounding success of their first cooperation.

Jan Friso highlighted the successful cooperations with industry within the Laquso project. (See here for more information.)

Hubert Garavel (HG) stated there are three necessary conditions for a successful collaboration with industry. The company should have

1. a strong interest in quality,
   
2. a lot of money and
   
3. a formal modelling group in house.
   

These criteria are difficult to find in a small- or medium-size company. In particular, the third criterion above is useful because it opens up the possibility of embedding a company engineer within the academic research group.

Is there any need for stochastic and probabilistic modelling in applications? More pointedly, have you met an example that you could not model because your tool does not support stochastic or probabilistic phenomena?

There seemed to be a general opinion here that probabilistic modelling is nice, but not necessary. More precisely, none of the speakers had yet met an example that they could not model adequately because their models and tools do not permit stochastic or probabilistic modelling.

JFG stated that he wants to work on research topics that can have applicability in real-life scenarios. He wants to have interaction with industry mainly as a way to learn what are the good/bad aspects of his modelling language and his tools. He feels that one should push for the use of the same model for verification and performance evaluation. (I have a vague recollection that this opinion was also shared by Kim.)

How can we, as a community, foster the building of industrial-strength tools based on sound theories?

The general feeling amongst the panelists was that our community does not have the infrastructure to support tooling efforts. HG pointed out how the situation is better in France, where the development of tools and languages is supported and recognized by institutions like INRIA. (My note: In hindsight, this is reflected by the success of long-term efforts like those that led to Esterel, Coq and CAML, amongst others.)

The panelists suggested that conferences and journals should be keener to accept tools and case studies as refereed contributions on a par with papers. JFG pointed out that Science of Computer Programming has now a track devoted to "expositions on implementations of and experiments with novel programming languages, systems and methods." The journal's web page also states that "It must be emphasized that papers describing new software tools of relevance to SCP are welcome under the strict condition that the source code of the tools is open." KGL also stated that the TACAS conference series was initiated precisely to give more visibility to tooling efforts in our community.

For a one-slide viewpoint on the economics of tool development look at slide 72 of Kim's presentation at the workshop.

What has concurrency theory offered industry so far? What are the next steps that the concurrency community should take in order to increase the impact of its research in an industrial setting? And what are future promising application areas for concurrency research?


JFG: Theory does not have much to offer to industry. We should probably view concurrency theory as a nice mathematical theory that need not have any real-world application.

As for what is it that we can do as a CONCUR community to assist in the work on tools, JFG's answer is to organize that as many students are being taught their use and effective application as possible. One of the biggest problems that we are facing is that far too few people in industry understand what formal methods and their tools can effectively bring to industry. To be on the safe side, they do not see where the techniques are effective and what they offer. They however understand that there are other pressing needs to invest time in.

If we teach formal methods we should teach the most advanced ones that the students can swallow. If they understand the advanced methods they can apply the more straightforward techniques. Of course the reverse does not hold. Don't teach them UML and expect them to understand mCRL2. But if you teach them mCRL2, they will not have any conceptual difficulty to apply UML.

KGL: We should make our techniques fit into the whole system-development process. We should also make sure that existing model-based tools that are already in use by industry have much stronger semantic foundations.

HG: Our community is in trouble! The model of concurrency that is prevalent is industry is Java-like (threads and shared variables). Our foundational beliefs are exotic for industry and message-passing, as used in our process calculi, is not the order of the day. Our major challenge is in pushing the clean model of concurrency we like. Every computer science department in every university should play its part in achieving this aim. Education is one of our best weapons to make industry accept our models and the techniques based upon them.

Concurrency Column for October 2007

I have just posted the piece that will appear in the concurrency column for the October 2007 issue of the BEATCS. The article, authored by Sergio Maffeis, is entitled Dynamic Web Data and Process Calculi and reports on the use of concepts and techniques from process calculi in the study and analysis of dynamic data.

Enjoy it.

Rance Cleaveland's Answers

It is a great pleasure for me to post some answers by my old mate Rance Cleaveland to the questions raised at the CONCUR workshop. Thanks to Rance for sharing his experience with us!


What an interesting workshop; I deeply regret not being able to attend.

At Luca's gentle suggestion ;-) I thought I would have a go at questions he posed at the end of his post.


What is the role/importance of real-time in modelling? Does industry want dense-time or discrete-time models?


In my experience with Reactis, my company's testing and verification tool, Reactis customers absolutely need real-time support. This is due to their applications, which are in automotive and aerospace and develop embedded control software. The most widely used commercial modeling languages (Simulink, Stateflow, SCADE) also include real-time as an intrinsic part of their semantics.

Ironically, given the sound and fury in the academic community, the industrial people I have interacted with for the most part do not care whether time is discrete or continuous. Sometimes, I have encountered customers who want to do hybrid-systems style modeling, and for these people continuity is important.


How does one involve small- and medium-size companies in collaborations with concurrency theoreticians/practitioners? Does "company size" matter?



Regarding SMEs (small- and medium-size enterprises ... a common acronym among US policymakers): I think the best way to involve them is via projects funded by third parties (governments, or a large partner). SMEs generally don't have the overheads to support "blue-sky" research, and their investment-return horizons are necessarily of shorter duration. At both Reactive Systems and Fraunhofer, our concurrency-oriented SME collaborations have either involved collaborations on government research grants or project work on behalf of larger customer. In the latter cases, it was important that we work in commercial notations (e.g. Simulink) rather than research-oriented ones.

Large companies do have resources to put into more basic research, but there is another phenomenon to be aware of: researchers in these companies often view outside researchers as competitors for their internal research funds. So collaborations with these organizations are highly dependent on the personal connections between company and non-company researchers. So-called "business unit" personnel are often the easiest to deal with, but in this case there needs to be a clear, typically short-term, pay-off to them for the collaboration.


Is there any need for stochastic and probabilistic modelling in applications? More pointedly, have you met an example that you could not model because your tool does not support stochastic or probabilistic phenomena?


We support simple probabilistic modeling in Reactis in the form of probability distributions over system inputs that we sample when creating tests. This feature, however, is almost never used by our customers. The reasons for this mostly boil down to a lack of training these engineers receive in stochastic modeling and control, which in turn is tied into the lack of good (or maybe standard) theory for stochastic differential equations.

More precisely, the engineers in automotive and aero that I've dealt with are usually mechanical or electrical engineers with backgrounds in control theory. The feedback control they use relies on plant models (i.e. "environments") being given as differential equations, which are deterministic. The plant models they devise for testing their control-system designs often have parameters that they tweak in order to test how their ideas work under different conditions.

These engineers talk in the abstract about how useful it would be to develop analytical frameworks for probabilistic plants, but tractable theories of probability spaces of differential equations are unknown, as far as I can tell.


How can we, as a community, foster the building of industrial-strength tools based on sound theories?


To have an industial following, tools have to work with languages that industry uses. For most research tools this is a problem, because the input languages are typically invented by the tool developers.

I see two possibilities. One is to work on commercial languages such as Simulink. These languages are often a catastrophe from a mathematical perspective, but they also usually contain subsets that can be nicely formalized for the purposes of giving tool support. If tools have a nice "intermediate notation" into which these cores can be translated, then this offers a pathway for potential industrial customers to experiment with the tools.

The second approach is to become involved in standardization efforts for modeling languages. UML 2.0 has benefited to some extent from concurrency theory, but there are many aspects of that language that remain informal and imprecise.


What has concurrency theory offered industry so far? What are the next steps that the concurrency community should take in order to increase the impact of its research in an industrial setting? And what are future promising application areas for concurrency research?


I think the best way to answer first question is to "trace backward" from commercial tools / modeling languages that have some basis in concurrency. Such tools would include those based on Statecharts (Stateflow, STATEMATE, BetterState); others based on Message Sequence Charts (Rational Rose, other UML tools); the French synchronous-language tools (SCADE, Esterel); tools that include model checkers (the EDA = "electronic design automation" industry); tools that use model-checking-base ideas for other analyses (Reactis, DesignVerifier).

Unfortunately the process-algebra community has had relatively little impact on commercial tool development. This is not due to shortcomings in the theory, in my opinion, but in the inattention that compositionality continues to receive in the (non-research) modeling community. In my experience, event-based modeling is also relatively uncommon, at least in auto and aero: sampling of "state variables" is the preferred modeling paradigm.

I personally would like to see work on semantically robust combinations of specification formulas (e.g. MSCs + state machines, or temporal logic + process algebra) and related tools; theoretically well-founded approaches to verifying systems that use floating-point numbers; and compositional, graphical modeling languages (lots of work done already, but still no commercial interest).

Moshe Vardi's Answers

Moshe Vardi has kindly sent me some brief answers to the questions I posted yesterday. I post them here in order to foster further discussion, and thank Moshe for his contribution.

• What is the role/importance of real-time in modelling? Does industry want dense-time or discrete-time models?

Moshe: Complex hardware designs today are locally synchronous, but globally asynchronous. Using multiple clocks to specify temporal properties is very
important, but I personally saw, so far, no application that required
dense-time reasoning. (Perhaps timing analysis of circuits requires dense
time?)

• How does one involve small- and medium-size companies in collaborations with concurrency theoreticians/practitioners? Does "company size" matter?

Moshe: Large companies can afford to think longer term and invest in internal/external research. This is quite harder to do with small companies, which typically looks for immediate solutions to their problems.

• Is there any need for stochastic and probabilistic modelling in applications? More pointedly, have you met an example that you could not model because your tool does not support stochastic or probabilistic phenomena?

Moshe: I have not seen it so far, but I do hear people starting to talk about probabilistic behavior of computer circuits. Perhaps we'll see a growing need for stochastic modeling in a few years.

• How can we, as a community, foster the building of industrial-strength tools based on sound theories?

Moshe: Academia can rarely build industrial-strength tools. Academic tools are
often the work of a single graduate student. Industry can put several PhD-level people on a single project.

• What has concurrency theory offered industry so far? What are the next steps that the concurrency community should take in order to increase the impact of its research in an industrial setting? And what are future promising application areas for concurrency research?

Moshe: IMHO, the biggest successes of the concurrency-theory community, broadly
conceived, is model checking and the development of synchronous languages. At the same time, many research direction in concurrency theory, such as process calculi and bisimulation theory have had fairly minimal impact. The theory community is often attracted to research based on its theoretical appeal, which does not always correlate with its industrial applicability. This does not mean that industrial applicability should be the guiding principle of research. Nevertheless, it would be worthwhile to pause once in a few years and examine the potential applicability of
theoretical research.

Report on the WG1.8 Workshop at CONCUR 2007---Part 1

Preface

As you may know, Jos Baeten, Wan Fokkink, Anna Ingolfsdottir, Uwe Nestmann and I organized a Workshop on Applying Concurrency Research in Industry, co-located with CONCUR 2007 in Lisbon, on behalf of WG1.8. The workshop was held on the afternoon of Friday, 7 September, and ran concurrently with the last two sessions of the main conference. Despite the competition with CONCUR, we had about 25 participants at the workshop, including several members of the working group. I think that this was a rather decent level of attendance for a "strategic event".

In this post, for the benefit of the WG members and of the community as a whole, I'll try to summarize the main discussion points that were raised during the presentations at the workshop and the ensuing panel discussion. I will also try to recall some of the questions that the audience asked the panel members. I hope that some of blog readers will want to contribute their opinion on these points and give their own answers to those questions themselves.

The organizers of the workshop will use all of the contributions that they'll receive in putting together an article for the concurrency column of the BEATCS.

Report on the Invited Talks

Note: I encourage the speakers to correct anything they said that I may have misinterpreted or misrepresented. I take full responsibility for any error I might have made in relaying the gist of the invited talks, and I'll be happy to post corrections and further comments. This is meant to be a live repository.

The workshop began with four invited presentations delivered by Hubert Garavel, Vincent Danos, Kim G. Larsen and Jan Friso Groote.

Hubert gave an overview of his twenty-year work on the CADP tool set, which is the oldest concurrency-theoretic tool still in activity. A thread underlying his work in what he called "applied concurrency theory" is that one must push the main results of our research area to industry and that this is only possible with the development of strong tool support for our methods. Hubert said that one of his design principles has been to restrict the tool's functionality for efficiency reasons, and that elegant semantics and efficient execution are two separate (at times conflicting) issues.

I have a note to the effect that, during Hubert's presentation, somebody (possibly Hubert himself) said that a lot of code doing bisimulation minimization has been lost over the years. We simply have not been consistent enough in preserving some of our earlier tooling efforts for the present generations of developers. Jan Friso said that current bisimulation minimization algorithms do not scale up to the size of the systems that are currently being analyzed, and asked whether it would be appropriate to rekindle research and implementation efforts on efficient and scalable bisimulation algorithms.

Earlier that day, Vincent had delivered an inspiring tutorial on his work in doing rule-based analysis of biological signalling. Listening to his tutorial, I was left with the impression that he is really having an impact in the life sciences, and that experimental biologists might very well use his tools based on concurrency-theoretic ideas. At the workshop, Vincent presented another way in which concurrency-theoretic ideas can help experimental biologists in their work. Experimental biology has a huge knowledge representation problem. (Vincent mentioned that there are two papers published in that area each minute!) In his opinion, experimental biologists can/should

• use concurrency-inspired languages to express biological understanding and
  
• display this information in a wiki-type system.
  

This will allow them to construct models systematically and to simulate them (exploiting the executable nature of concurrency-theoretic models) well beyond what is possible today by means of experiments.

Kim's talk was based on his experience with the ten-year development of the Uppaal tool, and reported on the knowledge transfer activity, which is part of his involvement in CISS. Apart from surveying the development of Uppaal and its recent offsprings, Kim's talk sent out the following general messages to the audience.

• Tools are a necessary condition for the successful transfer of concurrency-theoretic ideas in industry. Tool development is labour intensive, and one needs the sustained effort of many people over many years to produce good software tools.
  
• Academic courses offered to students and to industry practitioners play a key role.
  
• Concurrency researchers should try and target different communities of potential users. One never knows where successful applications are going to stem from.
  
• A good beginning is useful! Being able to start with a success story may lead to further successes and a long-term collaborations. However, Kim warned against assuming that a good beginning is a guarantee of a good ending, and recounted the story of the Aalborg collaboration with Bang and Olufsen, who disappeared from sight after Klaus Havelund, Arne Skou and Kim found and fixed a bud in one of their protocols. See here.
  
• The success of CISS shows that several companies are very interested in applying concurrency-theoretic ideas and tools because this reduces time to market and increases the quality of their products.
  
• The impact of one's work on the application of concurrency-theoretic research in industry is not always directly proportial to the amount of effort one puts into the work itself. Kim gave the example of the synthesis of control software controlling the temperature and humidity in an actual pig stable in Denmark. This software was synthesized using Uppaal Cora in a short time and is actually running to the satisfaction of its customers :-)
• Finally, Kim called for an expansion of the use of concurrency theory. We should link our work to testing, optimization etc. and embed it into standard software engineering methodologies, which are familiar to practitioners.
  

Jan Friso presented an overview of the mCRL2 tool set, and gave a demo of several features of the system. He stated his belief that proving the correctness of systems by hand gives one understanding that mere button-press model-checking does not yield. However, one needs tools to transfer knowledge to industry and to validate one's manual verifications. He also shared Hubert's belief that the initial emphasis on abstract data types in CADP and muCRL2 was a mistake, but that formalisms supporting data are necessary in applications. One of Jan Friso's messages was that high-performance in tools is underestimated, and that achieving it requires a lot of subtle work. Jan Friso also stressed the importance of teaching courses to our students that involve modelling and analysis of real-life industrial case studies. In that way, when students go and work in industry they will know that there are effective modelling languages and tools that they can use efficiently to check their designs before implementing them. He also stressed the importance of visualization tools.

Some Questions to the Speakers

Here are some questions that were addressed to the speakers during the panel discussion, in no particular order. I encourage readers of this report to post their own answers and further questions as comments to the post. Later on, I will post the answers from the panel members as I recall them.

• What is the role/importance of real-time in modelling? Does industry want dense-time or discrete-time models?
• How does one involve small- medium-size companies in collaborations with concurrency theoreticians/practitioners?
• Is there any need for stochastic and probabilistic modelling in applications? More pointedly, have you met an example that you could not model because your tool does not support stochastic or probabilistic phenomena?
• How can we, as a community, foster the building of industrial-strength tools based on sound theories?
• What has concurrency theory offered industry so far? What are the next steps that the concurrency community should take in order to increase the impact of its research in an industrial setting?

I hope that you will contribute your own questions to the above list and share your answers with the rest of the community via this blog. I will soon post some of the answers given by our panel at the workshop.

Addendum 14/9/2007: After I wrote this post, it occurred to me that the workshop discussion may have given the impression that industrial impact can solely be achieved by means of tools and joint case studies. Moshe Vardi's work on specification languages like ForSpec on the other hand indicates that the development of theoretically sound and clean specification languages that are actually used by industry is another area in which in the community can (and I believe should) have an impact.
I hope I can quote Moshe as saying
"In fact, I believe that much of my industrial impact has been achieved through the development of clean and useful theory."

CALCO Report, Part 3

This is the third, and final, installment of the coverage of CALCO 2007 on this blog. Thanks again to Mohammad for providing reports on the first three days of the event.

The first talk on Thursday was an invited address by Barbara König. Barbara's talk gave an excellent introduction to the general ideas and results on an active area of research in concurrency theory, namely the problem of deriving labelled transition system semantics and bisimulation congruences from reduction semantics and rewrite rules. This is a line of research that has been motivated by the theory of bisimulation congruences for process calculi, most notably the pi-calculus, and where categorical techniques play a fundamental role. See, for instance, the work by Leifer and Milner, and that by Sassone and Sobocinski.

Thursday also featured some talks on modal and epistemic logics, two talks on Chu spaces, and several categorical talks, which were alas well beyond my understanding of category theory.

The invited talk on Friday was delivered by Luis Caires, one of the prime movers behind the development of spatial logics. Luis' talk introduced a logical approach to the semantics of types for concurrency and to their soundness proofs based on spatial logics. I found the ideas presented in Luis' talk very intriguing, and I am going to read his paper in the proceedings when I have some time on my hands.

The conference concluded with a session on process algebra, where both Mohammad and I gave talks. (It is not for me to comment on how successful we were :-)) In case anybody is interested, the slides for my talk are here.

I enjoyed my trip to lovely Bergen, and thank the organizers for a very well-organized event. I hope to be able to visit Bergen again in the future. You can see some photos from Bergen here. Eventually, photos from CALCO will be available here.

Let me conclude with a couple of quotes from talks given at the conference and a poem I saw engraved in Vaagsallmenningen in Bergen.

"If you spell out this definition set theoretically, it looks quite horrible, but is not so difficult." (Clemens Kupke)

"The real voyage of discovery consists not in seeking new landscapes, but in having new eyes." (Marcel Proust, cited by Radu Mardare)

"Hele sit liv,
Anicet,
skal et menneske
laere at leve.
Hele sit liv,
Anicet,
skal han og
laere at doe."

(This roughly means "All his life, Anicet, a man must learn how to live. All his life, Anicet, he must also learn how to die.")