Publication

Stepwise refinement of formal specifications based on logical formulae

Related publications (114)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Modeling Consensus in a Process Calculus

Rachele Fuzzati, Massimo Merro

We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors; we use our model to formally prove that the algorithm satisfies its spec ...

2003

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications

Felix Gaertner

The tolerance theory by Arora and Kulkarni views a fault-tolerant program as the composition of a fault-intolerant program and fault tolerance components called detectors and correctors.At its core, the theory assumes that the correctness specifications un ...

2003

Towards the Formal Integration of Two Upcoming Standards: IEC61970 and IEC61850

Otto Preiss, Christian Frei, Tatjana Kostic

AbstractThe constant demand for a better integration of utility applications and systems provokes the question on the compatibility of standards that were, and still are, developed for these individual utility disciplines. This paper discusses the need for ...

2003

Monitoring of Resource Consumption in Java-based Application Servers

To realize dependable and profitable information and communication systems, computing resources (CPU, memory, network bandwidth) should be taken into account to a much wider extent than they are today. E-commerce infrastructure, such as application servers ...

2003

Mining Specifications

James Richard Larus

Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread ado ...

ACM2002

OS Support for P2P: a Case for TPS

Rachid Guerraoui, Patrick Eugster

Just like Remote Procedure Call (RPC) turned out to be a very effective OS abstraction in building client-server applications over LANs, Type-based Publish-Subscribe (TPS) can be viewed as a high-level candidate OS abstraction for building Peer-to-Peer (P2 ...

2002

OS Support for P2P Programming: a Case for TPS

Rachid Guerraoui, Patrick Eugster

Just like Remote Procedure Call (RPC) turned out to be a very effective OS ab-straction in building client-server applications over LANs, Type-based Publish-Sub-scribe (TPS) can be viewed as a high-level candidate OS abstraction for building Peer-to-Peer ( ...

2002

A Formal Analysis of Syverson`s Rational Exchange Protocol

Jean-Pierre Hubaux, Levente Buttyan, Srdan Capkun

In this paper, we provide a formal analysis of a rational exchange protocol proposed by Syverson. A rational exchange protocol guarantees that misbehavior cannot generate benefits, and is therefore discouraged. The analysis is performed using our formal mo ...

2002

From Formal Specifications to Ready-to-Use Software Components: The Concurrent Object-Oriented Petri Net Approach

Stanislav Chachkov

CO-OPN (Concurrent Object Oriented Petri Net) is a formal specification language for modelling distributed systems; it is based on coordinated algebraic Petri nets. In this paper we describe a method for generating an executable prototype from a CO-OPN spe ...

IEEE Computer Society Press2001

Abstractions for Distributed Programming: Guests or Relatives?

Rachid Guerraoui, Patrick Eugster, Christian Heide Damm

What abstractions are useful for expressing distributed interaction? This question has constituted an active area of research in the last decades and several candidates have been proposed, including remote method invocation, tuple spaces and publish/subscr ...

2001