Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Z notation

Related publications (9)

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Decentralized in-order execution of a sequential task-based code for shared-memory architectures

Charly Nicolas Lucien Castes

The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC). Sequential task-based programming models paired with adv ...

IEEE COMPUTER SOC2022

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

Declarative Specification and Alignment Verification of Services in ITIL

Alain Wegmann, Gil Regev

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

Formal semantics for refinement verification of entreprise models

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

Refinement Propagation. Towards Automated Construction of Visual Specifications

Alain Wegmann

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

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

Alain Wegmann, 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

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

A system engineering methodology integrating performance evaluation and formal specification

The situation of telecommunications systems is rapidly evolving towards a state characterized by the presence of a multitude of services integrated in a single network structure. In order to ease their integration, it is important to provide an unambiguous ...

EPFL1996

Related publications (9)