Browse Proceedings

In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool UPPAAL. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint ...

Safety is a system property and software, of itself, cannot be safe or unsafe. However software has a major influence on safety in many modern systems, e.g. aircraft and engine controls, railway signalling, and medical equipment.The paper outlines the ...

This work presents some methodologies for enhancing predictability in real-time computing systems, where explicit timing constraints have to be enforced on application processes. In order to provide an off-line guarantee of the critical timing ...

The UML (Unified Modeling Language) is a third-generation object-oriented modeling language recently accepted as a standard by the OMG (Object Management Group). The OMG is an association of over 800 leading technology companies that have banded ...

We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many initialization circularities that are missed by the standard lazy ...

From the first introduction of the notion of "Reactive Systems" and development of specification languages (such as Temporal Logic and Statecharts) and verification methods for this class of systems, it has been stated that this notion encompasses a ...

We describe formal verification of some of the key algorithms in the Time-Triggered Architecture (TTA) for real-time safety-critical control applications. Some of these algorithms pose formidable challenges to current techniques and have been formally ...

The controller synthesis paradigm provides a general framework for scheduling real-time applications. Schedulers can be considered as controllers of the applications; they restrict their behavior so that given scheduling requirements are met.We study a ...

Standardized and reusable software (SW) objects (or SW components - in-house or pre-fabricated) are increasingly being used to reduce the cost of software (SW) development. Given that the basic components may not have been developed with dependability ...

This paper introduces and formalizes a new variant of Timed Automata, called Time Labeled Scheduling Automata. A Time Labeled Scheduling Automaton is a single clock implementation model expressing globally the time constraints that a system has to meet. ...

We propose models that capture the influence of computation on the performance of computer-controlled systems, and make it possible to employ computational considerations in early stages of the design process of such systems. The problem of whether it ...

We propose timed multiset rewriting as a framework that subsumes timed Petri nets and timed automata. In timed multiset rewriting, which extends multiset rewriting, each element of a multiset has a clock, and a multiset is transformed not only by usual ...

Past decade has witnessed a great advance in the field of dense-time formal methods for the specification, synthesis and analysis of real time systems. In this context timed automata and real-time temporal logics provide a simple, and yet general, way ...

We study the problem of fault-diagnosis in the context of dense-time automata. The problem is, given the model of a plant as a timed automaton with a set of observable events and a set of unobservable events, including a special event modeling faults, ...

In this paper we show how to translate bounded-length verification problems for timed automata into formulae in difference logic, a propositional logic enriched with timing constraints. We describe the principles of a satisfiability checker specialized ...

Following the recent successes of bounded model-checking, we reconsider the problem of constructing models of discrete-time Duration Calculus formulae. While this problem is known to be nonelementary when arbitrary length models are considered [Han94], ...

Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded ...

Most real-time systems require responsive interrupt handling. Programming of interrupt handlers is challenging: in order to ensure responsiveness, it is often necessary to have interrupt processing enabled in the body of lower priority handlers. It ...

We address the problem of verifying clique avoidance in the TTP protocol. TTP allows several stations embedded in a car to communicate. It has many mechanisms to ensure robustness to faults. In particular, it has an algorithm that allows a station to ...

The aim of conformance testing is to check whether an implementation conforms to a specification. We consider the case where the specification contains timing constraints and is described by a model called Timed Automata (TA). The state space of a TA ...

This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to ...

This paper concerns analyzing UML based models of distributed real time systems involving multiple active agents. In order to avoid the time-penalties incurred by distributed execution of synchronous operation calls, it is typically recommended to ...

We describe a prototype tool, HUGO/RT, that is designed to automatically verify whether the timed state machines in a UML model interact according to scenarios specified by time-annotated UML collaborations. Timed state machines are compiled into timed ...

In a parallel composition of timed automata, some transitions are independent to others. Generally the basic method generates one successors for each of the legal permutations of the transitions. These successors may be combined into one bigger symbolic ...

A semantics for a graphical specification language of real-time properties (Constraint Diagrams) is presented. The new semantics is given in terms of Timed Automata. A model in terms of Timed Automata satisfies the property given by a Constraint Diagram ...