Publication

Exploiting Various Levels of Semantics in CO-OPN for the SANDS Environment Tools

Publications associées (58)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

From high-level component-based models to distributed implementations

Joseph Sifakis

Although distributed systems are widely used nowadays, their implementation and deployment is still a time-consuming, error-prone, and hardly predictive task. In this paper, we propose a methodology for producing automatically efficient and correct-by-cons ...

ACM2010

On Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using r ...

2009

Constraint Solving for Software Reliability and Text Analysis

Viktor Kuncak

We will develop and implement new algorithms for constraint solving and apply them to construct two classes of tools: 1) bug finding and verification tools building on tools such as Java PathFinder and Jahob; 2) tools for deep semantic analysis of texts co ...

2008

An OCL Semantics Specified with QVT

Slavisa Markovic

Metamodeling became in the last decade a widely accepted tool to describe the (abstract) syntax of modeling languages in a concise, but yet precise way. For the description of the language's semantics, the situation is less satisfactory and formal semantic ...

2006

Looking Ahead in Open Multithreaded Transactions

Maxime Monod

Open multithreaded transactions constitute building blocks that allow a developer to design and structure the execution of complex distributed systems featuring cooperative and competitive concurrency in a reliable way. In this paper we describe an optimiz ...

2006

Integrating Shape Analysis into the Model Checker BLAST

Dirk Thilo Beyer, Grégory Théoduloz

Many software model checkers are based on predicate abstraction. Values of variables in branching conditions are represented abstractly using predicates. The strength of this approach is its path-sensitive nature. However, if the control flow depends heavi ...

2006

Validation of Visual Contracts for Services

Alain Wegmann, Lam Son Lê, José Diego de la Cruz Garcia

Visual modeling languages have specialized diagrams to represent behavior and concepts. This diagram specialization has drawbacks like the dif-ficulty to represent the effects of actions. We claim that visual contracts can de-scribe actions in a more compl ...

2006

VISUAL CONTRACTS: A way to reason about states and cardinalities in IT system specifications

Alain Wegmann, Lam Son Lê, José Diego de la Cruz Garcia

Visual modeling languages propose specialized diagrams to represent behaviour and concepts necessary to specify IT systems. As a result, to understand a specification, the modeller needs to analyze these two types of diagrams and, often, additional stateme ...

2006

Lazy Shape Analysis

Dirk Thilo Beyer, Grégory Théoduloz

2005

Generation of object-oriented programs from CO-OPN specifications

Stanislav Chachkov

The execution of formal specifications is important for verification, validation and animation purposes. This thesis describes transformation of CO-OPN specifications in executable code. The original goal of this transformation was validation by prototypin ...

EPFL2004