Concurrency Theory IFIP WG1.8

IFIP 1.8 workshop on FORMAL METHODS FOR EMBEDDED SYSTEMS

2009-10-12T09:16:00.000Z

Here is the call for participation for an event organized the WG. Do take part if you happen to be in Eindhoven for FM week!

========================================
CALL FOR PARTICIPATION
========================================
IFIP 1.8 workshop on FORMAL METHODS FOR EMBEDDED SYSTEMS

http://www.cse.unsw.edu.au/~rvg/FMES/

Eindhoven, The Netherlands, November 5, 2009
======================================================================

This IFIP 1.8 workshop is organised as part of the Formal Methods Week,
which takes place in Eindhoven from November 2 until November 6, 2009.
The goal of the workshop is to summarise research from different areas
of formal methods targeted to embedded systems, and to promote the use
of formal methods in different applications and in the engineering
discipline for embedded systems.

PROGRAMME:
----------
8:30 Registration and coffee
8:50 Opening

9:00 Bert van Beek -
The Compositional Interchange Format: concepts, formal basis,
and applications
9:45 Holger Hermanns -
Synchronous vs. Asynchronous Performance Models of Industrial
Networks on Chip Designs

10:30 Coffee break

11:00 Catuscia Palamidessi -
Synchronization in the pi-calculus
11:45 Joost-Pieter Katoen -
Analysis and Semantics of Extended AADL Models

12:30 Lunch
14:00 The End

For abstracts of the talks and further details about the workshop we
refer to http://www.cse.unsw.edu.au/~rvg/FMES/.

REGISTRATION
------------
The registration fee for the workshop is 45 euros and covers coffee/tea
and lunch. You also need to register for FMweek, which costs an
additional 35 euros (administration costs). Please register via the
FMweek website: http://www.win.tue.nl/fmweek

WORKSHOP ORGANISERS:
---------------------
Rob van Glabbeek (National ICT Australia)
Ursula Goltz (Technical University Braunschweig, Germany)
Bas Luttik (Technische Universiteit Eindhoven, The Netherlands)
Uwe Nestmann (Technical University Berlin, Germany)

Vardi Receives The Blaise Pascal Medal in Computer Science For 2008

2008-09-25T15:10:00.002Z

I just learned that WG1.8 member Moshe Vardi is the recipient of the Blaise Pascal Medal in Computer Science for 2008 of the European Academy of Sciences. This is outstanding news for TCS as a whole and for our WG in particular.

The motivation for the prize reads:

In recognition of his outstanding contributions in several areas of computer science connected by their use of logic as an underlying methodology. His work has had fundamental and lasting impact on automatic verification, logic of knowledge, database theory, and finite-model theory.

Congrats to Moshe!

Changes at the helm of WG1.8 and plans for the near future

2008-09-09T06:41:00.002Z

I apologize for not posting much on this blog of late. Life has been very hectic and the organization of ICALP 2008 took its toll on me, but that's no excuse for the silence.

Chairpersons of IFIP WGs are in service for a three-year period and may apply for reappointment for another three-year stint. My period of service is running out as we speak and, in the light of several other family- and work-related commitments, I think that it is best for the WG if I step down as chair now. The WG needs a more active and visible chairperson. Thanks a lot for your cooperation over the last three years. I enjoyed it a lot.

Wan Fokkink and Anna Ingolfsdottir will also step down from their positions as vice-chair and secretary of the WG. Thanks a lot to them for their sterling service.

The IFIP secratariat will organize an election that will allow us to decide on our new chairperson democratically. We are lucky to have a strong candidate for the role, namely Jos Baeten. Jos is the chairman of the Steering Committee for CONCUR and the Dutch national representative within TC1. If he is elected as chairperson of the WG, he will therefore ensure a seamless integration of our activities with those within the CONCUR conferences and within TC1.

If you would like to run for election, please drop me a line.

We are also planning several new strategic workshops under the auspices of the WG. We will organize a workshop affiliated with FM 2009, which will be held in Eindhoven. The workshop will be organized by Wan Fokkink and Uwe Nestmann, and its preliminary theme is related to the connections between the research carried out within the CONCUR community and the PODC community, with possible emphasis on the development of verification techniques and tools.

We are also thinking about organizing a workshop at CONCUR 2009 in Bologna. We already have some ideas for possible topics for the workshop, but we welcome your input for this and future workshops.

I also encourage you to use the blog for airing your opinions, questions and desires related to the activities of the WG.

I'll sign off now, since Tim Roughgarden is starting his invited talk at TCS 2008.

ICALP 2008

2008-07-14T13:19:00.002Z

ICALP 2008 is now over. We had nearly 500 people attending the main conference and its affiliated events. It was a lot of work to organize such a large scientific meeting, but Anna, Magnús and I were very happy to see that people enjoyed their visit to Iceland and their stay in Reykjavík.

Here I will limit myself to giving a few remarks on the last three days of the ICALP conference.

On Wednesday, Bruno Courcelle (Labri, Universitè Bordeaux, France) delivered a plenary invited talk entitled Graph Structure and Monadic Second-order Logic: Language Theoretical Aspects. Courcelle is one of the 15 most cited French scientists and the most cited French computer scientist. (See http://www.labri.fr/perso/courcell/PrixCitations2004.doc.) In addition, he has become a member of the very prestigious Institut Universitaire de France (see http://iuf.amue.fr/author/bcourcelle/). Courcelle is one of the grand "old" men in theoretical computer science. In a career spanning about 35 years he has given fundamental contributions to the study of the logical, language-theoretic and algorithmic aspects of the theory of graphs. He is also one of the founders of, and main contributors to, algebraic semantics. In his talk, Bruno described the role that hierarchical decompositions and Monadic Second-order Logic play in the extension of methods and results from classic Formal Language Theory to the description of sets of finite graphs. Bruno is putting the final touches to a monograph on this topic that will be published by Cambridge University Press. (Present state of the work Part 1 : Chapters 1-6. Part 2 : Chapters 7-11.)

The scientific programme on Thursday was kicked off by an invited plenary talk by Peter Winkler (Dartmouth, USA). The talk, entitled Optimality and Greed in Dynamic Allocation, described a method for proving optimality in dynamic allocation problems that relies on the assumption that "it's right to be greedy." The method was developed while Peter was working on two problems which arose at Lucent Technologies.

The scientific programme for Thursday reached its climax with the award ceremony, during which the EATCS award and the Gödel prize where handed out. After receiving the EATCS award, Leslie G. Valiant (Harvard, USA) delivered an excellent 30-minute presentation focusing on three topics that interest him right now. The topics are:

Evolution
Intelligence
Human Brain.

In his opinion, all these topics are computer science and are screaming for an understanding based on algorithmic approaches. Leslie described some of his work in this direction.

The Gödel prize talk, delivered by Daniel A. Spielman (Yale, USA), provided an outstanding finale for the day. In his talk, Dan explained the idea of smooth anallysis, how Teng and he thought of it and what he hopes the future will bring. Shang-Hua Teng (Boston University, USA) gave a personal and heartfelt introduction to the work they did to merit such a prestigious award.

The main event during the final day at ICALP was an invited plenary talk delivered by Javier Esparza (Technische Universität München, Germany). Javier's presentation was entitled Newtonian Program Analysis and presented recent work by his students and him that aims at using a computational approach to solving equations developed by Isaac Newton about 300 years ago in the analysis of computer programs. The talk presented exciting work and was beautifully and enthusiastically delivered. After the talk, Peter Winkler commented to us: "You saved the best for the last!" Javier closed the talk by saying that "Newton did it all 300 years ago, but he never saw Iceland!"

ICALP 2009 will be held in Rhodos, Greece. Good luck to the organizers of ICALP 2009!

Frits Vaandrager's Answers

2007-10-06T22:49:00.000Z

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

2007-10-05T22:03:00.000Z

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

Luca de Alfaro in the News

2007-09-24T07:55:00.000Z

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 :-)

Guest Post from Jorge Perez

2007-09-22T13:18:00.000Z

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

2007-09-21T16:46:00.000Z

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 laboratory. (See here for more information.)

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

a strong interest in quality,
a lot of money and
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.

Moshe Vardi's Answers

2007-09-14T10:38:00.000Z

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

2007-09-13T15:00:00.000Z

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 bug 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 proportional 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 scope for 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 muCRL 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- and medium-size companies in collaborations with concurrency theoreticians/practitioners? Does "company size" matter?
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? And what are future promising application areas for concurrency research?

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 members 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."

Call for Participation: CONCUR Workshop

2007-07-15T07:15:00.000Z

The details of the programme of the workshop the WG is organizing at CONCUR are now available here. I hope that many of you will be able to attend and to contribute to the discussion. The workshop organizers are also planning a special issue of a journal devoted to theme of the workshop, and I trust that several of you will want to submit papers to it.

Members of the WG are also organizing other events affiliated with CONCUR. These are:

Expressiveness in Concurrency (EXPRESS). Organizers: Roberto Amadio and Thomas Hildebrandt, 3rd September 2007.

Security Issues in Concurrency (SECCO). Organizers: Daniele Gorla and Catuscia Palamidessi, 3rd September 2007

Enjoy.

CONCUR Workshop Proposal Accepted

2006-12-05T08:41:00.000Z

The title of the post says it all. Further details will be posted on this blog as soon as possible. For the moment, I can tell you that Hubert Garavel has accepted to deliver one of the addresses at the workshop, and that we are contacting two or three more speakers.

Make plans to attend the workshop!

WG Workshop at CONCUR 2007 (Proposal)

2006-11-21T11:25:00.000Z

FYI, here is the workshop proposal that we sent to the CONCUR organizers. If it gets accepted, then we hope that this will be the first of a series of strategic meetings for the WG.

--------------------------------------------------

TITLE: IFIP WG 1.8 Workshop on Applying Concurrency Research in Industry (7 or 8 September 2007)

DURATION: Half a day

ORGANIZERS: Luca Aceto, Jos Baeten, Wan Fokkink, Anna Ingolfsdottir, and Uwe Nestmann (on behalf of WG1.8)

SUMMARY: This strategic workshop, held under the auspices of IFIP Working Group 1.8 on Concurrency Theory, aims at highlighting the challenges that arise in applying concurrency theory research in an industrial setting, broadly construed. Its purpose is to be a forum for the discussion of the state-of-the-art in the transfer of results from concurrency theory to industry, and for distilling the lessons to be learned from the successes and failures so far. Moreover, we shall discuss, e.g., how to increase the impact that concurrency research can have in industry, the role of software tools in this technology transfer effort, and what are possible novel industrial application areas of concurrency theory research. The ultimate goal of the meeting, and subsequent discussions, will be to establish road map(s) for the concurrency theory community, or parts thereof, in applying its research in industrial settings.

The topic of the workshop is strongly related to all of the areas of CONCUR interest. Semantics, logics, and verification techniques for concurrent systems are necessary for the development of languages and methods for use in industrial applications. Conversely, the industrial applications of methods from concurrency theory research stimulate further advances in the basic theory covered by the CONCUR conference series. Successful applications of concurrency theory in industry further highlight the fundamental scientific and technological relevance of work done within the CONCUR community.

SELECTION OF PAPERS: The workshop will consist of three-four invited presentations, followed by discussions. We might summarize the presentations and discussions in an article for the concurrency column of the Bulletin of the EATCS. The theme of the workshop could form the basis for a special issue of a journal (for instance JLAP), but such a special issue would not be necessarily based upon presentations at the workshop. There would be a separate call for contributions for that volume.

millions of loc in the pi-calculus (or any process algebras).

2006-11-13T01:22:00.000Z

I was thinking of writing on this blog for a long time since I heard it had been opened, but failed to see some basic things such as how to login. Now I leaned it from Luca, and I will write a few lines.

In this first entry, I wish to write about programs. There are many programs in the world, open source or closed source. There are hundreds of programming languages, and millions lines of C code for systems level programming, and millions lines of applications code. Some of them form the infra of computing. And software lives long, often longer than machine architecture. No ISAs I know of have the instruction for "while", but it continues to be used surviving all different ISAs, now or in future. That is software.

Over the last decades, Internet and world wide web became new computing reality, and open source has initiated a new way to build software infrastructure. During this period I have been studying process algebras, together with the colleagues in the community. What has this activity been? We have surely been working on general theories, but we have also been working on description of processes, small or large, chaotic or well-behaved. So we have also been programming. Programming in processes, which have almost always been abstract, but still building behaviour, just as practical programmers do with C, Java, etc. And there are so many behaviours interacting processes can realise (starting from vendor machines to SKI combinators to file servers to data structures to Turing machines to higher-order functions to objects to cryptographic protocols to biological processes).

As I wrote, ours has so far been programming in the abstract. Through recent dialogues with people in industry, however, I have come to realise a strange thing: it looks that in all areas of programming, from embedded software to OS programming to servers to application integration, what I got trained as abstract programming is becoming reality. Why? For a simple reason that there is an increasing need to describe interacting processes: this is so when we wish to make clear in what ways complex long-term financial transactions involving many parties can be stipulated so that every party is sure how one should behave; when we need be sure that a networking product from one software vendor is interoperable with one from a different software vendor, based on information disclosed by them; or when we wish to run a program really fast in a multicore processor, making the best of its on-chip interconnect; or when we wish to do a complex mash-up of many web services to create a richer service; when we wish to contol mobile devices which get spontaneously engaged in many kinds of high-level interactions.

All this has been more or less out there for some time, or at least in preparation. But they are now getting visible and gathering pace.

I have had chances to talk with those industry people who are in dire needs to obtain and work with such interactions. For example a chief software architect in a major international bank told me that he needs to have a complete grasp of how thousands of applications in different departments in his bank interact with each other as a whole, describe and manage it (he is finding a suitable language for doing this). When I listened to his story, what I saw in my mind's eye is millions of lines of the pi-calculus processes in action. Surely the pi-calculus in particular and process algebras in general are too fine-grained for describing application-level interactions: their setup is aimed at distilling fundamental concepts, for developing basic theories. And yet what this architect should be having in near future are nothing but description of communicating processes. These interacting software should be developed rapidly, safely upgraded and incremented at run-time (without worries on deadlock, livelock, lack of compatibility, violation of regulation, etc.), usable for decision-making, and should be manageable. In short, we need description, analysis and control.

These description and analysis are nothing but part of what we have been doing in process theories, albeit in the abstract. And our inquiries into basic theory will continue, since I am afraid we have only touched its surface. Yet even from our study so far, we know several basic things about how to treat interacting processes. For example we know that it is hard even to understand what it means that two processes behave in the same way. Now thousands of programmers are going to program behaviours of such processes. What are communicating processes that I am writing? What is their behaviour, and how can I organise them?

I deem the coming interaction between engineering and theory to be a non-trivial and rich one. Many elements will make this collaboration far from straightforward and, at the same time, thrilling. It will pose many interesting questions. Today I have written long enough (I was thinking only a paragraph is enough). In a near future, we may be able to come back to this blog and discuss a couple of concrete problems picked up in my recent interactions with the engineering world.

kohei

Workshop on Emerging Trends in Concurrency Theory

2006-11-11T10:16:00.000Z

The colloquium Emerging Trends in Concurrency Theory will be held at LIX, École Polytechnique de Paris, during 13-15 of November 2006. The colloquium is organized by Catuscia Palamidessi and Frank D. Valencia, and will be held under the auspices of Working Group 1.8 on Concurrency Theory of IFIP TC1. The guest of honor will be Turing Award winner Robin Milner, who was awarded one of the prestigious Blaise Pascal International research chairs to visit LIX for the 2006-2007 academic year.

The event will have well over 10o participants, and has a programme of talks to whet anybody's appetite. I am really sorry to have to miss this event, which clashes with the exams for our courses in Reykjavík---a rather mundane reason for having to miss what will be a great event.

Fortunately, Wan (Fokkink), the co-chair of WG1.8, will be there, you will be able to discuss with him matters related to the proposal to hold a WG workshop at CONCUR 2007.

It would be great if one or more of you could report on the workshop using the blog. I, for one, would be happy to read about yet another great event I am missing.

CONCUR 2007 Workshop?

2006-10-26T16:52:00.000Z

Antonio Ravara just posted an announcement on the Types mailing list asking for workshop proposals in connection with CONCUR 2007 in Lisbon. (See also here.)

In his comment to my previous post, Jos Baeten wrote:

I think it is a good idea to have a one-day WG 1.8 workshop at each CONCUR conference, with a short WG meeting at the end of it.

Shall we submit a WG1.8 workshop proposal? If so, who would like to be involved in the PC? What kind of workshop shall we aim at, an informal meeting or one with proceedings? The deadline mentioned in Antonio's message and on the workshops web page is November 24, 2007---but I assume that he means 2006 :-)---so we have to move quickly.

The notification of acceptance is due on December 4, 2007 (again 2006, I presume).

If I do not receive enough reactions via the comments section of the blog, I'll resort to emailing to reach an agreement fast.

Two Possible Discussion Items

2006-09-19T17:07:00.000Z

I was wondering whether we should have a concurrency report series like the Electronic Colloquium on Computational Complexity, which has been going strong for over ten years now. Would there be added value in having a repository of that type, where full versions of concurrency-related papers are posted? If so, where should it located? At DBLP/Trier?

Also, what should the connection between the WG and the CONCUR conference series be? Should we make a point of organizing a (possibly informal) meeting at each CONCUR conference? Or should we aim at organizing affiliated workshops at CONCUR?

Addendum: Luca Trevisan mentioned the existence of this blog on his excellent blog in theory. I therefore took the opportunity of asking his readers about the value of the Electronic Colloquium on Computational Complexity for the complexity theory community. It'll be good to have them contribute their experiences to this discussion---a case of volume A-volume B communication :-)

I have joined.

2006-09-18T06:09:00.000Z

Luca,
I have joined the blogging service!
Don't have anything clever to say at teh moment.
Thiagu.

Open Problems and Future Research Directions Repository

2006-09-13T08:11:00.001Z

This is the first post on this experimental blog for the IFIP WG1.8 on Concurrency Theory. We invite members of the concurrency theory community to participate in the discussions raised on this blog by sending their comments/suggestions/thoughts using the commenting feature of the blogging system.

Let us assume that one can assess the healthiness of concurrency theory by looking at the most important open problems in that field. These open problems can be used to try and convince researchers in another area and students that the field of concurrency theory is "alive and kicking", and maybe entice a few of them to work within the field.

Based upon this thought experiment, wouldn't it be a good thing to have a repository of open problems that identify the present state of development in concurrency theory, and suggest directions for further research?

At some point in the past, I started putting together a list of open problems, but I have not maintained it for a while. Will you help me revive this enterprise by sending me, or posting as a comment to this blog entry, a description of your favourite open problems in concurrency theory, together with links to partial solutions and pointers to the literature? This input of yours might even form the basis for a useful installment of the Concurrency Column in the Bulletin of the EATCS (which I could edit on behalf of the contributors), and generate a lot of research in our field.

I also believe that the result of this discussion would be useful for the whole concurrency theory community.