Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument. In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are rejected by the standard projection. The key to the new projection is an analysis that tracks causality between messages. Our soundness proof uses novel graph-theoretic techniques from the theory of message-sequence charts. We demonstrate the efficacy of the new projection operation by showing many global types for common patterns that can be projected under our projection but not under the standard projection operation.

We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.

We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.

We introduce a visual notation for local specification of concurrent components based on message sequence charts (MSCs). Each component is a finite-state machine whose actions are MSCs that specify its local view of the overall communication in the system. These local MSCs are composed into coherent global scenarios using a separately specified set of transactions. Intuitively, each MSC represents a phase of interaction. We introduce a mechanism to overlap phases that allows complex interactions to be specified without obscuring the logical structure of the constituent scenarios. Our notation combines the global view available in models such as high-level message sequence charts (HMSCs) with the local, asynchronous structure captured by message-passing automata (MPA). In fact, both HMSCs and MPAs can be captured as special cases of our formalism. In this paper we focus on the syntax and formal semantics of our notation, with examples that illustrate why this approach is more natural for capturing real-life specifications. We also describe an approach to use automated tools to analyze systems specified using our notation.

This volume contains the proceedings of the 28th international conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), organized under the auspices of the Indian Association for Research in Computing Science (IARCS). This year's conference attracted 117 submissions. Each submission was reviewed by at least three independent referees. The final selection of the papers making up the programme was done through an electronic discussion on EasyChair, spanning two weeks, without a physical meeting of the Programme Committee (PC). All PC members participated actively in the discussion. We have five invited speakers this year: Hubert Comon-Lundh, Uriel Feige, Erich Graedel, Simon Peyton Jones and Leslie Valiant. We thank them for having readily accepted our invitation to talk at the conference and for providing abstracts (and even full papers) for the proceedings. We thank all the reviewers and PC members, without whose dedicated effort the conference would not be possible. We thank the Organizing Committee for making the arrangements for the conference. This year, the conference is being held at the Indian Institute of Science, Bangalore, as part of its centenary year celebrations. It is a great honour and privilege for the conference to be recognized and associated with the institute on this occasion. Finally, this year we have taken a decisive step in democratizing the conference by moving away from commercial publishers. Instead, we will be hosting the proceedings online, electronically, via the Dagstuhl Research Online Publication Server (DROPS). A complete copy of the proceedings will also be hosted on the FSTTCS website (www.fsttcs.org). The copyrights to the papers will reside not with the publishers but with the respective authors. The copyright is now governed by the Creative Commons attribution NC-ND. We do hope this direction will be sustained in the future.

This volume contains the proceedings of the 28th international conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), organized under the auspices of the Indian Association for Research in Computing Science (IARCS).

The only practical way to test distributed message-passing systems is to use local testing. In this approach, used in formalisms such as concurrent TTCN-3, some components are replaced by test processes. Local testing consists of monitoring the interactions between these test processes and the rest of the system and comparing these observations with the specification, typically described in terms of message sequence charts. The main difficulty with this approach is that local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking for implied scenarios is known to be undecidable for regular specifications, even if observations are made for all but one process at a time. We propose an approach where we append tags to the messages generated by the system under test. Our tags are generated in a uniform manner, without referring to or influencing the internal details of the underlying system. These enriched behaviours are then compared against a tagged version of the specification. Our main result is that detecting implied scenarios becomes decidable in the presence of tagging.