Publication

Modelling and verification of a multiprocessor realtime OS kernel

Related publications (34)

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.

Lazy Shape Analysis

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 ...

2005

Debugging Temporal Specifications with Concept Analysis

James Richard Larus

Program verification tools (such as model checkers and static analyzers) can find many errors in programs. These tools need formal specifications of correct program behavior, but writing a correct specification is difficult, just as writing a correct progr ...

ACM2003

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

A Formal Specification for a Real-Time Train Controller

Simon Kramer

We give a formal specification for a real-time controller for trains that operate on the Italian railway network. The controller will control train movements and is part of a larger system destined to guarantee safety with respect to dangers originating fr ...

2001

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

The TL Compiler

This paper describes a method of compiling specification properties into automata or test oracles which allow testing of any proposed implementation. It also shows how to interpret the automata's status during testing. The method addresses verification of ...

2000

Developing safe concurrent and distributed applications with an architectural environment

The developing environment presented in the paper is built around an interactive tool that can accompany the software engineer for the whole software development process of concurrent and distributed applications. This environment relies on a concept of ac ...

IEEE Comput. Soc1999

Stepwise refinement of formal specifications based on logical formulae

One of the steps making it possible to increase the quality and the reliability of the software executing on distributed systems consists of the use of methods of software engineering that are known as formal. The majority of the formal methods currently e ...

EPFL1999

Stepwise Refinement of Formal Specifications Based on Logical Formulae: from COOPN/2 Specifications to Java Programs

1999

Formal testing of object-oriented software

Cécile Peraire

This thesis presents a method and a tool for test set selection, dedicated to object-oriented applications and based on formal specifications. Testing is one method to increase the quality of today's extraordinary complex software. The aim is to find progr ...

EPFL1998