ETD system

Electronic theses and dissertations repository


Tesi etd-05232016-100710

Thesis type
Tesi di dottorato di ricerca
Specification and Verification of Contract-Based Applications
Settore scientifico disciplinare
Corso di studi
tutor Prof. Degano, Pierpaolo
tutor Prof. Ferrari, Gian Luigi
Parole chiave
  • choreography
  • orchestration
  • formal methods
  • service composition
  • automata
  • model-checking
  • verification
Data inizio appello
Riassunto analitico
Nowadays emerging paradigms are being adopted by several companies, where applications<br>are built by assembling loosely-coupled distributed components, called services.<br>Services may belong to possibly mutual distrusted organizations and may have conflicting<br>goals. New methodologies for designing and verifying these applications are<br>necessary for coping with new scenarios in which a service does not adhere with its<br>prescribed behaviour, namely its contract.<br>The thesis tackles this problem by proposing techniques for specifying and verifying<br>distributed applications. The first contribution is an automata-based model checking technique<br>for ensuring both service compliance and security requirements in a composition of<br>services. We further develop the automata-based approach by proposing a novel formal<br>model of contracts based on tailored finite state automata, called contract automata.<br>The proposed model features several notions of contract agreement described from a<br>language-theoretic perspective, for characterising the modalities in which the duties and<br>requirements of services are fulfilled. Contract automata are equipped with different<br>composition operators, to uniformly model both single and composite services, and techniques<br>for synthesising an orchestrator to enforce the properties of agreement. Algorithms<br>for verifying these properties are introduced, based on control theory and linear programming<br>techniques. The formalism assumes the existence of possible malicious components<br>trying to break the overall agreement, and techniques for detecting and banning eventually<br>liable services are described. We study the conditions for dismissing the central<br>orchestrator in order to generate a distributed choreography of services, analysing both<br>closed and open choreographed systems, with synchronous or asynchronous interactions.<br>We relate contract automata with different intutionistic logics for contracts, introduced<br>for solving mutual circular dependencies between the requirements and the obligations of<br>the parties, with either linear or non-linear availability of resources. Finally, a prototypical tool implementing the theory developed in the thesis is presented.