PhD in Computer Science

Specifying Stateful Asynchronous Properties for Distributed Programs

Academic year 2013/2014

Sommario del corso

• Course objectives
• Notes
• Teaching tools

Course objectives

Abstract: Having stateful specifications to track the states of processes, such as the balance of a customer for online shopping or the booking number of a transaction, is needed to verify real-life interacting systems. For safety assurance of distributed IT infrastructures, specifications need to capture states in the presence of asynchronous interactions. We demonstrate that not all specifications are suitable for asynchronous observations because they implicitly rely on an order-preservation assumption. To establish a theory of asynchronous specifications, we use the interplay between synchronous and asynchronous semantics, through which we characterise the class of specifications suitable for verifications through asynchronous interactions. The resulting theory offers a general semantic setting as well as concrete methods to analyse and determine semantic well-formedness (healthiness) of specifications with respect to asynchronous observations, for both static and dynamic verifications. In particular, our theory offers a key criterion for suitability of specifications for distributed dynamic verifications.

Class schedule

Note

TEACHER:

Dott. Tzu-Chun Chen, Queen Mary university

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums