AMAST Mail 1996
[Prev][Next][Index]

PhD thesis available

Dear all,

this message is to announce the availability of my PhD Thesis. I report
below the title, a brief abstract and the table of contents of the thesis.
Hard copies can be obtained by sending a request to
        priami@di.unipi.it.

An electronic copy can be obtained by anonymous ftp at
        ftp.di.unipi.it
in the directory
        \pub\Papers\priami\
The file is
        PhD.ps.Z.

Best wishes,

Corrado Priami

=========================================================================

Author: Corrado Priami
Title: Enhanced Operational Semantics for Concurrency
Institution: Dipartimento di Informatica, Universita` di Pisa
Address: Corso Italia, 40
         I-56125 Pisa - Italy
Numero: TD-08/96
Abstract:
In this study we extend the classical structural operational semantics to
implement the possibility of having different views of the same system
that are all consistent to one another and that can be recovered
mechanically from a single, concrete representation.
We apply this idea to concurrent and distributed systems, and especially
to mobile agents.

Our concrete representation is a transition system (called
proved and defined in SOS style),
whose transitions are labelled by encodings of their deduction
trees. The labels of transitions allow us to retrieve all the
main semantic models presented in the literature
and also to define new semantics (e.g. a new causality). These
semantics are retrieved from the proved transition system
through relabelling functions that only maintain
the relevant information in the labels of transitions.
We show that our approach is robust:
it scales up smoothly to higher-order process calculi and even to real
programming languages like Facile. Its applicability is made
evident through an example of debugging of Facile
``real code'' for an application on mobile agents.

To automate the above
approach for verification of distributed systems, we study the
state explosion problem. We overcome it for languages that
do not contain scope operators like CCS
restriction. Under this assumption we obtain a compact proved transition
system that is linear (in average) with the occurrences of actions in a
process and that preserves non interleaving bisimulation-based
equivalences (thus checked in polynomial time instead of exponential one).
We describe two prototypes that allow their user to change easily from a
semantic model to another.

We also study the refinement of specifications towards real code.
Since implementations must meet performance constraints, we first enhance our
proved semantics to derive from it stochastic models on which performance
can be evaluated. We also show how it is possible to merge semantic
descriptions
with information on architecture topologies in order to get evaluations
that are more accurate as machine sensible. Along this line, we
describe how to refine proved semantics in order to avoid global manager
of names in distributed systems. The resulting description is actually a
specification for distributed name managers that could help improving
distributed implementations.


Table of Contents:

1 Introduction...............................................13
        1.1  Formal methods..................................14
        1.2  Operational semantics...........................16
        1.3  Abstraction levels..............................22
        1.4  Computer aided verification.....................30
        1.5  Towards implementations.........................35
        1.6  Suitability of SOS as formal method.............41
        1.7  Outline of the work.............................42
        1.8  The origins of the chapters.....................45
2.  Mathematical Background..................................49
        2.1  Mathematical Logic..............................49
        2.2  Sets............................................54
        2.3  Relations and Functions.........................57
        2.4  Frequently used structures......................59
        2.5  Algebra.........................................60
        2.6  Complete partial orders.........................64
        2.7  Formal Languages................................66
        2.8  Continuous time Markov chains...................70
3.  Structural Operational Semantics.........................73
        3.1  Transition systems..............................73
        3.2  SOS definitions.................................78
4.  Semantics for Concurrency................................81
        4.1  Pi-calculus.....................................81
        4.2  Higher order Pi-calculus........................89
        4.3  Facile..........................................90
5.  Proved Transition System................................105
        5.1  Proved operational semantics...................105
        5.2  Properties.....................................110
        5.3  Finite branching early semantics...............112
        5.4  An Algebra of Proved Trees.....................117
6.  Non Interleaving Semantics..............................121
        6.1  Non interleaving relations.....................122
        6.2  Causality......................................127
        6.3  Locality, Precedence and Enabling..............135
        6.4  Independence...................................142
        6.5  Concurrency....................................143
        6.6  Equivalences...................................154
        6.7  Higher-Order Mobile Processes..................161
        6.8  Related Works..................................163
        6.9  The causal transition system...................169
7.  Partial Ordering Semantics..............................175
        7.1  Partial and mixed orderings....................176
        7.2  po relabelling.................................178
        7.3  mo vs. po semantics............................181
        7.4  SOS po semantics...............................183
        7.5  Proof of Theorem 7.3.1.........................184
8.  A Case Study: Facile....................................191
        8.1  Proved Transition System.......................192
        8.2  Causality......................................204
        8.3  Locality.......................................207
        8.4  Examples.......................................209
        8.5  Analysis of a Mobile File Browser Agent........213
9.  Extended Transition Systems.............................225
        9.1  Parametric bisimulation........................226
        9.2  Observations and regular languages.............233
        9.3  PisaTool.......................................236
10. Complexity and Concurrency..............................243
        10.1 Why Complexity and Concurrency.................244
        10.2 The scenario...................................245
        10.3 Complexity of a semantic model.................250
        10.4 Event structures and Petri nets................254
        10.5 No free lunches................................255
11. Compact Representations.................................259
        11.1 Compact transition systems.....................260
        11.2 SOS generation.................................278
        11.3 Related work...................................286
12. YAPV....................................................289
        12.1 Relabelling functions..........................289
        12.2 Generalizing bisimulation......................292
        12.3 Implementation of YAPV.........................296
13. Stochastic Pi-calculus..................................307
        13.1 The stochastic extension.......................307
        13.2 Performance measures...........................312
        13.3 An example.....................................314
        13.4 Topologies.....................................315
        13.5 Some remarks...................................321
14. A Distributed Name Manager..............................325
        14.1 Handling names.................................325
        14.2 A router.......................................328
        14.3 Operational semantics..........................331
Conclusions.................................................343
References..................................................347

============================================================================


&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&

   Corrado Priami
   Universita' di Pisa                  Tel.: +39 (0)50 887268
   Dipartimento di Informatica          Tlx.: 590291 DIPISA I
   Corso Italia, 40                     Fax:  +39 (0)50 887226
   I-56125 PISA, Italia
[ AMAST Mail 1996 | Latest Update | AMAST Mail Meta-Index | AMAST ]