Timed control with observation based and stuttering invariant strategies. (2008)
Cassez, Franck, David, Alexandre, Larsen, Kim, Lime, Didier, Raskin, Jean-François
In this paper we consider the problem of controller synthesis for timed games under imperfect information. Novel to our approach is the requirements to strategies: they should be based on a...
Timed control with observation based and stuttering invariant strategies. (2008)
Cassez, Franck, David, Alexandre, Larsen, Kim, Lime, Didier, Raskin, Jean-François
In this paper we consider the problem of controller synthesis for timed games under imperfect information. Novel to our approach is the requirements to strategies: they should be based on a...
Marie-Claire, Cynthia, Salzmann, Julie, David, Alexandre, Courtin, Cindie, Canestrelli, Corinne, Noble, Florence
Drugs of abuse induce alterations in cytoskeletal and cytoskeleton associated genes in several brain areas. We have previously shown that acute MDMA regulates the mRNA level of Rnd3, a Rho GTPase...
Marie-Claire, Cynthia, Salzmann, Julie, David, Alexandre, Courtin, Cindie, Canestrelli, Corinne, Noble, Florence
Drugs of abuse induce alterations in cytoskeletal and cytoskeleton associated genes in several brain areas. We have previously shown that acute MDMA regulates the mRNA level of Rnd3, a Rho GTPase...
Características clínicas do osteossarcoma na infância e sua influência no prognóstico (2004)
Rech,Ângela, Castro Jr,Cláudio G, Mattei,Jane, Gregianin,Lauro, Di Leone,Luciane, David,Alexandre, ...
OBJETIVOS: Conhecer as características clínicas e determinar os fatores de importância prognóstica de crianças e adolescentes com osteossarcoma. MATERIAIS E MÉTODOS: Foram revisados os...
Modelling and Analysis of a Commercial Field Bus Protocol (2003)
We report on an industrial application of UPPAAL, in which a commercial field bus protocol (AF100) is modelled and analysed using the tool. During the case study, a number of imperfections in the...
Unification & Sharing in Timed Automata Verification (2003)
Alexandre David, Gerd Behrmann, Kim G. Larsen, Wang Yi
We present work on unifying the two main data structures involved during reachability analysis of timed automata. We also present result on sharing common elements between states. The experimental...
UPPAAL Implementation Secrets (2002)
Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, Wang Yi
In this paper we present the continuous and on-going development of datastructures and algorithms underlying the veri cation engine of the tool Uppaal. In particular, we review the datastructures of...
Formal Verification of UML Statecharts with (2002)
Alexandre David, M. Oliver Moller, Wang Yi
We present a framework for formal verification of a realtime extension of UML statecharts. For clarity, we restrict ourselves to a reasonable subset of the rich UML statechart model and extend this...
Practical Verification of Real-Time Systems (2001)
Formal methods are becoming mature enough to be used on non trivial examples. They are particularly well fitted for real-time systems whose correctness is defined in terms of correct responses at...
Formal Verification of UML Statecharts with Real-time Extensions (2001)
Alexandre David, M. Oliver Moller, Wang Yi
We present a framework for formal verification of a real-time extension of UML statecharts. This formalism is based on hierarchical state machines, that can be put in parallel at any level of...
Tools for Real-Time UML: Formal Verification and Code Synthesis (2001)
Tobias Amnell, Alexandre David, Elena Fersman, M. Oliver Moller, Paul Petterson
We present a real-time extension of UML statecharts to enable modelling and verification of real-timed constraints. For clarity, we shall consider a reasonable subset of the rich UML statechart model...
RS-01-11 David M oller: From Hierarichcal Timed Automata to UPPAAL (2001)
Alexandre David, M. Oliver M Oller
We present a hierarchical version of timed automata, equipped with data types, hand-shake synchronization, and local variables. We describe the formal semantics of this hierarchical timed automata...
Alexandre David, M. Oliver M Oller
We present a hierarchical version of timed automata, equipped with data types, hand-shake synchronization, and local variables. We describe the formal semantics of this hierarchical timed automata...
UPPAAL - Now, Next, and Future (2001)
Pedro R. D'argenio, Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Alexandre David, Ansgar Fehnker, ...
Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The...
UPPAAL - Present and Future (2001)
Gerd Behrmann, Alexandre David, Kim G. Larsen, Paul Pettersson, Wang Yi
Uppaal is a tool for modelling, simulation and verication of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool...
Modelling and Analysis of a Commercial Field Bus Protocol (2000)
We report on an industrial application of UPPAAL, in which a commercial field bus protocol (AF100) is modelled and analysed using the tool. During the case study, a number of imperfections in the...
Hierarchical Timed Automata for UPPAAL (1999)
In recent years, there have been a number of model-checking tools developed for timed automata. A common problem with these tools is that they can only accept a collection (or a product) of automata...
Protocol Verification using UPPAAL: Exercises (1999)
This note describes a serie of exercises on Uppaal. It is recommended to solve them in groups of two students. The purpose of the exercise is to demonstrate how behaviours can be modeled in CCS, and...
UL++. an Object Oriented Language for Hiearchical Modeling and Analysis (1999)
Syntax We define an abstract syntax to describe in a compact manner our control structure hierarchy. S' refers to a general state, which can be a superstate or a simple node (N). The arrow s,,,'>...
Bania, Jacek, Gatti, Evelina, Lelouard, Hugues, David, Alexandre, Cappello, Fanny, Weber, Ekkehard, ...
MHC class II-restricted antigen presentation plays a central role in the immune response against exogenous antigens. The association of invariant (Ii) chain with MHC class II dimers is required for...
Bania, Jacek, Gatti, Evelina, Lelouard, Hugues, David, Alexandre, Cappello, Fanny, Weber, Ekkehard, ...
MHC class II-restricted antigen presentation plays a central role in the immune response against exogenous antigens. The association of invariant (Ii) chain with MHC class II dimers is required for...
Lelouard, Hugues, Ferrand, Vincent, Marguet, Didier, Bania, Jacek, Camosseto, Voahirana, David, Alexandre, ...
In response to inflammatory stimulation, dendritic cells (DCs) have a remarkable pattern of differentiation (maturation) that exhibits specific mechanisms to control antigen processing and...