LASER Summer School on Software Engineering

» Software engineering for concurrent and real-time systems « 

September 11 - 17, 2005
Elba, Italy

Director: Bertrand Meyer (ETH Zürich)

  Home | Topics | Speakers | Lectures | Schedule | Other activities | Visitor Information | Contacts | Registration | Pictures | Previous LASER school  
 

Lectures

Title: A process-algebra for web computing

Speaker: Jayadev Misra

Description: The computational pattern inherent in many wide-area applications is this: acquire data from one or more remote services, calculate with these data, and invoke yet other remote services with the results. Additionally, it is often required to invoke alternate services for the same computation to guard against service failure. It should be possible to repeatedly poll a service until it supplies results which meet certain desired criteria, or to ask a service to notify the user when it acquires the appropriate data. And it should be possible to download an application and invoke it locally, or have a service provide the results directly to another service on behalf of the user.

We introduce site as a general term for a basic service. A web service is a site. More generally, a distributed transaction, which can be regarded as an atomic step of a larger computation, is a site.

We call the smooth integration of sites orchestration, and Orc is our theory of orchestration of sites. Orchestration requires a better understanding of the kinds of computations that can be performed efficiently over a wide-area network, where the delays associated with communication, unreliability and unavailability of servers, and competition for resources from multiple clients are dominant concerns.

Consider a typical wide-area computing problem. A client contacts two airlines simultaneously for price quotes. He buys a ticket from either airline if its quoted price is no more than $300, the cheapest ticket if both quotes are above $300, and any ticket if the other airline does not provide a timely quote. The client should receive an indication if neither airline provides a timely quote. Such problems are typically programmed using elaborate manipulations of low-level threads. We regard this as an orchestration problem in which each airline is a site; we can express such orchestrations very succinctly in Orc.

Our theory is built upon a small number of composition operators. We use an operator for parallel composition and one for sequential composition. And, we have an operator which allows selective pruning of parallel threads and data transfer across subcomputations. We show a variety of examples from web services and other domains to illustrate the power of these composition operators. Our theory is applicable to distributed application design in general, with particular emphasis on orchestration of web services.

Further reading:    

Slides: 1-2, 3, 4, 5, 6

Title: Szumo: a compositional contract model for safe multi-threaded applications

Speaker: Laura Dillon

Description: It is well known that the expressive power afforded by the use of concurrency comes at the expense of increased complexity. Without proper synchronization, concurrent access to shared objects can lead to race conditions, and incorrect synchronization logic can lead to starvation or deadlock. Moreover, concurrency confounds the development of reusable software modules because synchronization policies and decisions are difficult to localize into a single software module. A module can implement a synchronization policy that satisfies safety and liveness requirements in some usage contexts but that fails to satisfy the same requirements in other contexts. We believe the safe and reliable use of concurrency in multi-threaded shared-memory systems is a fundamental and pervasive engineering concern, and deserves the same level of attention and support as more traditional safety, efficiency, and scalability concerns.

Szumo (Synchronization Units Model) extends an object-oriented language with a notion of synchronization contracts to address these concerns. In lieu of writing low-level code to acquire and release shared objects, programmers declare synchronization contracts in a module's interface. These contracts declare the circumstances under which modules require exclusive use of shared objects in a form that permits automated inference of how to synchronize processes in using these objects. A distributed run-time scheduler negotiates the contracts on behalf of processes, ensuring that the contracts of all modules are met while simultaneously guarding against data races and avoidable deadlocks. Separating concurrency concerns from functional code simplifies programming, and localizing concurrency concerns in module interfaces simplifies reasoning.

We have prototyped Szumo in Ruby and incorporated it fully into Eiffel. Currently, we are incorporating it into C++ and investigating how synchronization contracts can be used synergistically with traditional design methods and formal analysis techniques to provide stronger safety and reliability guarantees. This series of lectures provides an introduction to Szumo and describes current research activities aimed at enabling technology transfer. We examine a case study to validate the efficacy of Szumo on a realistic design problem: the component-based design of a multi-threaded web server.

Lectures:

  1. Introduction to Szumo
  2. Case Study: A contract-aware web server using contract-unaware libraries
  3. Case Study: Extending the web server to allow dynamic content
  4. Case Study: Replacing a module to allow load balancing
  5. Comparison with other concurrency models
  6. Ongoing and future work on contract models

Further reading:  

Slides: 1, 2, 3

Title: Component-based modeling of real-time systems

Speaker: Joseph Sifakis

Description: We present a framework for the construction of timed models for real-time systems, encompassing the following:

  • composition of heterogeneous components. Two deep sources of heterogeneity are identified: 1) heterogeneity of interaction and 2) heterogeneity of execution.
  • compositionality and composability rules for correctness by construction with respect to generic properties such as deadlock-freedom, timelock-freedom and liveness.
  • incremental construction. This is achieved by using a unique associative composition operator.

In the framework, component models consist of three distinct layers. The first layer describes the component's behaviour. The second layer is an interaction model which defines the possible interactions of the component. The third layer is a scheduler which applies a scheduling policy so as to meet given QoS requirements. The composition of two components is obtained by composing separately the corresponding layers.

We show how the proposed framework can be applied to build models of real-time systems. These are obtained by compositionally adding timing constraints to components of their application software. These constraints take into account execution times of atomic statements, the dynamics of the external environment, as well as quality of service requirements.

We illustrate applications of these results by using the IF modeling toolset by Verimag on which the framework has been partially implemented.

Further reading: 

  • Joseph Sifakis "Modeling real-time systems--challenges and work directions" EmSoft01, LNCS 2211, Tahoe City, October 2001.
  • J. Sifakis, S. Tripakis, S. Yovine "Building models of real-time systems from application software" Proceedings of the IEEE, Special issue on modeling and design of embedded systems, 91(1):100-111, January 2003.
  • K. Altisen, G. Goessler, J. Sifakis "Scheduler modeling based on the controller synthesis paradigm" Journal of Real-time Systems, Vol. 23, pp.55-84, 2002.
  • E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Vernier, D. Weil S. Yovine " TAXYS : a tool for the development and verification of real-time embedded systems " CAV01, LNCS 2102, Paris, July 2001.
  • C.Kloulinas, C. Nakhli, S. Yovine "A methodology and tool support for generating scheduled native code for real-time java applications" EmSoft03, LNCS 2855, pages 274-289. Philadelphia, October 2003.
  • G. Goessler, J. Sifakis. "Composition for Component-Based Modeling" Science of Computer Programming, vol. 55, pp. 161--183 (March 2005)
  • The IF toolbox http://www-verimag.imag.fr/~async/IF/index.shtml.en 

Slides: 1

Title: Object technology for concurrent and real-time programs

Speaker: Bertrand Meyer

Description:  Practitioners building concurrent, distributed, real-time applications need practical mechanisms to program at a sufficiently abstract level and guarantee a level of software quality at least comparable to what is achievable in sequential applications. This set of lectures will present a candidate for addressing this challenge: the SCOOP framework for concurrent, distributed and real time programming. The lectures will cover the rationale behind SCOOP, some of the theory, and extensive applications and examples. Students will have the opportunity to solve a number of problems.

Further reading: OOSC2 Chapter

Slides: 1, 2, 3

Title: Temporal verification of reactive programs

Speaker: Amir Pnueli

Description: These lecture series present a set of techniques for the verification of reactive and concurrent systems. We develop the theory leading to the case of infinite-states systems and the application of abstraction methods for their verification.

After introducing the computational model of Fair Discrete Systems (FDS) and the specification language of (linear) Temporal Logic (LTL), we present the main methods for the verification of temporal properties of reactive systems, which are Model Checking and Deductive Verification. The general approach to such verification is based on the construction of Temporal Testers.

To deal with infinite-state systems, we present a uniform approach to verification by Finitary abstraction. This is a method by which an infinite-state system is abstracted into a finite-state system which can then be model checked.

We begin by providing a general sound recipe for the finitary abstraction of a verification problem which jointly abstracts the system and its temporal specification. We show that Predicate Abstraction is a special case of this sound recipe.

We then show that state abstraction is not adequate for proving liveness properties by abstraction. We introduce the method of Augmented Finitary Abstraction, by which the system is augmented by a progress monitor prior to its abstraction. It is claimed that this extended method is complete for proving by abstraction any temporal property of an infinite-state systems.

We show that augmented abstraction is a practical approach to proofs of liveness properties, and is simpler to apply than corresponding deductive proofs which require the design of a full ranking function which decreases on every helpful step.

We illustrate the power of the programmable model checker TLV and demonstrate how it can be used for the automatic computation of abstracted systems. This includes an example of shape analysis by predicate abstraction.

Further reading:

Slides: 1, 2

Title: Transparent distribution of real-time software components based on logical execution time

Speaker: Wolfgang Pree

Description: Software components enable reuse in practice and improve software quality. Existing component models do not explicitly deal with time. The lecture introduces a component model for real time systems which covers this aspect and which also allows transparent component distribution. Transparent distribution means that (1) the functional and temporal behavior of a system is the same no matter where a component is executed and (2) the developer does not have to care about the differences of local versus distributed execution of a component.

The component model is based on the Logical Execution Time (LET) programming abstraction, which was invented in the Giotto project at the University of California, Berkeley and which abstracts from physical execution time and thereby from both the execution platform and the communication topology. A discussion of the resulting tool chain and component integration process rounds out the lecture.

Further reading:

Slides: 1, 2, 3

 

Chair of Software Engineering - ETH Zürich Last update: 1-September-2005