Publication

Animation-Based Service Specification, Verification and Validation

Publications associées (41)

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

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

Alignment Verification in the Early Stage of Service Design

Alain Wegmann, Gorica Tapandjieva Sekulovska, Matteo Filipponi

Verification is a costly task, sometimes burdensome and tedious, requiring strong formal background. To reduce the effort and cost invested in verification, we developed a model-driven approach for automatic verification of service properties, done in the ...

2017

Synthesizing robust systems

Barbara Jobstmann

Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if ass ...

Springer2014

Patterns for Value-Added Services Illustrated with SEAM

Maude Laetitia Grossan, Alain Wegmann, Gorica Tapandjieva Sekulovska, Aarthi Gopal

The basic idea behind the provision of a service is to hide the service implementation details from the client in such a way that more value is provided to the client. Very often support services allow too much of their implementation details to be visible ...

2014

Analog property checkers: a DDR2 case study

Dejan Nickovic

The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be in ...

Springer US2010

Model checking: Algorithmic verification and debugging

Joseph Sifakis

Turing Lecture from the winners of the 2007 ACM A.M. Turing Award.In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly succes ...

2009

Formal semantics for refinement verification of entreprise models

Irina Rychkova

In this dissertation we investigate how Business/IT alignment in enterprise models can be enhanced by using a software engineering stepwise refinement paradigm. To have an IT system that supports an enterprise and meets the enterprise business needs, manag ...

EPFL2008

Declarative Specification and Alignment Verification of Services in ITIL

Gil Regev, Alain Wegmann, Irina Rychkova

IT organizations that wish to implement the best practices recommended by the IT Infrastructure Library (ITIL) need to specify the level of service provided to their customers. The implemented service needs to comply with this specification. We propose a m ...

2008

Visual contracts (VCs)

José Diego de la Cruz Garcia

Model-Driven Engineering (MDE) harbors the promise of developing software-based systems with little or no coding. Instead of coding, it is envisioned that software engineers build models that are automatically translated into code. The modeling notation of ...

EPFL2008

Refinement Propagation. Towards Automated Construction of Visual Specifications.

Alain Wegmann, Irina Rychkova

Creation and transformation of visual specifications is driven by modeler’s design decisions. After a design decision has been made, the modeler needs to adjust the specification to maintain its correctness. The number of adjustments might make the design ...

2007