| [1] |
Philippe Bidinger and Adriana Compagnoni.
Pict correctness revisited.
2008.
Theoretical Computer Science. Coordination/FMOODS'07
Special Issue. This paper subsumes [4]. To appear.
[ bib |
.pdf ]
The Pict programming language is an implementation of the pi-calculus in which executions of pi-calculus terms are specified via an abstract machine. An important property of any concurrent programming language implementation is the fair execution of threads. After defining fairness for the pi-calculus, we show that Pict abstract machine executions implement fair pi-calculus executions. We also give new proofs of soundness and liveness for the Pict abstract machine.
|
| [2] |
Adriana Compagnoni, Elsa L. Gunter, and Philippe Bidinger.
Role-based access control for boxed ambients.
In Theoretical Computer Science. Festschrift in Honor of
Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca, Lecture Notes in
Computer Science, 2008.
To appear.
[ bib ]
In this paper we describe a calculus for mobile processes and propose a mechanism for specifying access privileges based on a combination of the identity of the users seeking access, their credentials, and the location from which they seek it, within a reconfigurable nested structure.
|
| [3] |
Ananda Basu, Philippe Bidinger, Marius Bozga, and Joseph Sifakis.
Distributed semantics and implementation for systems with interaction
and priority.
In Formal Techniques for Networked and Distributed Systems -
FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June
10-13, 2008, Proceedings, Lecture Notes in Computer Science, 2008.
[ bib |
.pdf ]
The paper studies a distributed implementation method for the BIP (Behavior, Interaction, Priority) component framework for modeling heterogeneous systems.
|
| [4] | Philippe Bidinger and Adriana B. Compagnoni. Pict correctness revisited. In Marcello M. Bonsangue and Einar Broch Johnsen, editors, Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings, volume 4468 of Lecture Notes in Computer Science, pages 206-220. Springer, 2007. [ bib | .pdf ] |
| [5] |
Philippe Bidinger, Matthieu Leclercq, Vivien Quéma, Alan Schmitt, and
Jean-Bernard Stefani.
Dream Types - A Domain Specific Type System for Component-Based
Message-Oriented Middleware.
In 4th Workshop on Specification and Verification of
Component-Based Systems (SAVCBS'05), in association with ESEC/FSE'05,
Lisbon, Portugal, 2005.
[ bib |
.pdf ]
We present a type system for the dream component-based message-oriented middleware. This type system aims at preventing the erroneous use of messages, such as the access of missing content. To this end, we adapt to our setting a type system developed for extensible records.
|
| [6] |
Philippe Bidinger, Alan Schmitt, and Jean-Bernard Stefani.
An abstract machine for the Kell calculus.
In Formal Methods for Open Object-Based Distributed Systems, 7th
IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, 2005,
Proceedings, volume 3535 of Lecture Notes in Computer Science, pages
43-58, Athens, Greece, June 2005.
Best Paper Award.
[ bib |
.pdf ]
The Kell Calculus is a family of process calculi intended as a basis for studying distributed component-based programming. This paper presents an abstract machine for an instance of this calculus, a proof of its correctness, and a prototype OCaml implementation. The main originality of our abstract machine is that it does not mandate a particular physical configuration (e.g.mapping of localities to physical sites), and it is independent of any supporting network services. This allows to separate the proof of correctness of the abstract machine per se, from the proof of correctness of higher-level communication and migration protocols which can be implemented on the machine.
|
| [7] |
P. Bidinger and J.B. Stefani.
The Kell Calculus: Operational Semantics and Type System.
In Formal Methods for Open Object-Based Distributed Systems, 6th
IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, 2005,
Proceedings, volume 2884 of Lecture Notes in Computer Science.
Springer, 2003.
[ bib |
.pdf ]
This paper presents the Kell calculus, a new distributed process calculus that retains the original insights of the Seal calculus (local actions, process replication) and of the M-calculus (higher-order processes and programmable membranes), although in a much simpler setting than the latter. The calculus is equipped with a type system that enforces a unicity property for location names that is crucial for the efficient implementation of the calculus.
|
This file has been generated by bibtex2html 1.85.