Publication

A system engineering methodology integrating performance evaluation and formal specification

Related publications (91)

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.

A platform for mixed HW/SW algorithm specifications for the exploration of SW and HW partitioning

Marco Mattavelli, Christophe Lucarz

The increasing complexity in particular of video and multimedia processing has lead to the need of developing the algorithms specification using software implementations that become in practice generic reference implementations. Mapping directly such softw ...

Springer-Verlag2007

Path invariants

Dirk Thilo Beyer

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In curr ...

2007

An Extensible and Personalized Approach to QoS-enabled Service Discovery

Karl Aberer, Manfred Hauswirth

We present an extensible and customizable framework for the autonomous discovery of Semantic Web services based on their QoS properties. Using semantic technologies, users can specify the QoS matching model and customize the ranking of services flexibly ac ...

2007

Distributed Consensus, Revisited

Rachele Fuzzati, Massimo Merro

We provide a novel model to formalize a well-known algorithm, by Chandra and Toueg, that solves Consensus among asynchronous distributed processes in the presence of a particular class of failure detectors (Diamond S or, equivalently, Omega), under the hyp ...

2006

Path Invariants

Dirk Thilo Beyer, Andrey Rybalchenko

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In ...

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

"Sentry Pallets" for Automated Monitoring of Spatial Constraints

Philippe Cudré-Mauroux

Warehouses must maintain a number of spatial constraints concerning the safe handling of hazardous materials. In this paper, we address the problem of automated monitoring of spatial constraints as pallets are moved on forklifts by human operators. We prop ...

2006

Expressing Systemic Contexts in Visual Models of System Specifications

Gil Regev, Alain Wegmann, José Diego de la Cruz Garcia

Decision support systems can be used to manage systems. Managed systems are described by system specifications. System specification notations, such as UML, often separate in different diagrams the static specification and the dynamic specification of the ...

2005

The KeY Tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an in ...

Springer2005

Detecting Malicious Code by Model Checking

Johannes Kinder

The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demons ...

Springer2005