%% inria-00507143, version 1
%% http://hal.inria.fr/inria-00507143/en/
@TechReport{rr7381,
author = {Bertrand, N. and Stainer, A. and Jéron, T. and
Krichen, M.},
title = {A game approach to determinize timed automata},
institution = {INRIA},
type = {Research Report},
year = 2010,
number = 7381,
month = {October},
abstract = {Timed automata are frequently used to model
real-time systems. Their determinization is a key
issue for several validation problems. However, not
all timed automata can be determinized, and
determinizability itself is undecidable. In this
paper, we propose a game-based algorithm which,
given a timed automaton, tries to produce a
language-equivalent deterministic timed automaton,
otherwise a deterministic over-approximation. Our
method subsumes two recent contributions: it is at
once more general than the existing determinization
procedure and more precise than the approximation
algorithm. Moreover, we explain how to extend our
method to deal with invariants and
$\varepsilon$-transitions, and also consider other
useful approximations: under-approximation, and
combination of under- and over-approximations.},
URL =
{http://hal.inria.fr/docs/00/52/48/30/PDF/RR-7381.pdf},
X-ID-HAL = {inria-00524830}
}
@techreport{k-opacity,
title = { {V}arious {N}otions of {O}pacity {V}erified and
{E}nforced at {R}untime},
author = {{F}alcone, {Y}. and {M}archand, {H}.},
abstract = {{I}n this paper, we are interested in the validation
of opacity where opacity means the impossibility for
an attacker to retrieve the value of a secret in a
system of interest. {R}oughly speaking, ensuring
opacity provides confidentiality of a secret on the
system that must not leak to an attacker. {M}ore
specifically, we study how we can verify and
enforce, at system runtime, several levels of
opacity. {B}esides already considered notions of
opacity, we also introduce a new one that provides a
stronger level of confidentiality.},
type = {Research Report},
institution = {INRIA},
number = 7349,
month = {August},
year = 2010,
URL = {http://hal.inria.fr/inria-00507143/PDF/RR-7349.pdf},
X-ID-HAL = {inria-00507143}
}
@inproceedings{FalconeRV10,
author = {Falcone, Y.},
title = {You should Better Enforce than Verify (Tutorial)},
booktitle = {RV'10: Proceedings of the 1st International
Conference on Runtime Verification},
year = 2010,
month = {November},
address = {Malta},
publisher = {Springer},
series = {LNCS},
volume = {6418},
pages = {89-105},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/tutorial-RV10-Falcone.pdf},
doi = {http://dx.doi.org/10.1007/978-3-642-16612-9},
abstract = {This tutorial deals with runtime enforcement which
is an extension of runtime verification aiming to
circumvent misbehaviors of programs. Within this
technique the monitor not only observes the current
program execution, but it also modifies it. It uses
an internal memory, in order to ensure that the
expected property is fulfilled: it still reads an
input sequence but now produces a new sequence of
events in such a way that the property is
enforced. The precise and formal relation between
input and output sequences is usually ruled by two
constraints: soundness and transparency. From an
abstract point of view those constraints entail the
monitor to minimally modify the input sequence in
order to ensure the desired property. This tutorial
focuses on runtime enforcement and advocates its use
as an extension to runtime verification. More
specifically the tutorial steps are the following:
1) we overview previous approaches to runtime
enforcement; 2) we thoroughly present our latest
advances in runtime enforcement that generalizes and
extends previous approaches; 3) we discuss practical
limitations and future challenges. },
X-ID-HAL = {hal-00523653},
x-international-audience ={yes},
x-proceedings ={yes}
}
@inproceedings{FalconeJaberSERP10,
author = {Falcone, Y. and Jaber, M.},
title = {Towards Automatic Integration of an Or-BAC Security
Policy Using Aspects},
booktitle = {World Comp 2010: Software Engineering Research and
Practice (SERP'10)},
address = {Las Vegas, USA},
month = {July},
year = 2010,
pdf = {http://hal.inria.fr/hal-00525490/PDF/sigproc-sp.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {hal-00525490}
}
@Article{Rusu10b,
author = {Egea, M. and Rusu, V.},
title = {Formal Executable Semantics for Conformance in the
MDE Framework},
journal = {Innovations in Systems and Software Engineering},
year = 2010,
pages = {73-81},
volume = 6,
doi = {http://dx.doi.org/10.1007/s11334-009-0108-1},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/rusu2010.pdf},
abstract = {In the MDE framework, a metamodel is a language
referring to some kind of metadata whose elements
formalize concepts and relations providing a
modeling language. An instance of this modeling
language which adheres to its concepts and relations
is called a valid model, i.e., a model satisfying
structural conformance to its metamodel. However, a
metamodel frequently imposes additional constraints
to its valid instances. These conditions are usually
written in OCL and are called well-formedness
rules. In presence of these constraints, a valid
model must adhere to the concepts and relations of
its metamodel and fullfill its constraints, i.e., a
valid model is a model satisfying semantical
conformance to its metamodel. In this work, we
provide a formal semantics to the notions of
structural and semantical conformance between models
and metamodels building on our previous work. Our
definitions can be automatically checked using the
ITP/OCL tool.},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{r10,
author = {Rusu, V.},
title = {Combining narrowing and theorem proving for
rewriting-logic specifications},
booktitle = {4th International Conference on Tests and Proofs
(Tap'10)},
month = {July},
year = 2010,
publisher = {Springer},
series = {LNCS},
volume = {6143},
pages = {135-150},
doi = {http://dx.doi.org/10.1007/978-3-642-13977-2_12},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2010-tap.pdf},
abstract = {We present an approach for verifying dynamic systems
specified in rewriting logic, a formal specification
language implemented in the Maude system. Our
approach is tailored for invariants, i.e.,
properties that hold on all states reachable from a
given class of initial states. The approach consists
in encoding invariance properties into inductive
properties written in membership equational logic, a
sublogic of rewriting logic also implemented in
Maude. The invariants can then be verified using an
inductive theorem prover available for membership
equational logic, possibly in interaction with
narrowing-based symbolic analysis tools for
rewriting-logic specifications also available in the
Maude environment. We show that it is possible, and
useful, to automatically test invariants by symbolic
analysis before interactively proving them. },
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{infinity10,
author = {Bertrand, N. and Morvan, C.},
title = {Probabilistic Regular Graphs},
booktitle = {Infinity},
series = {EPTCS},
pages = {77-90},
year = 2010,
volume = 39,
address = {Singapore},
month = {September},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2010-infinity.pdf},
doi = {http://dx.doi.org/10.4204/EPTCS.39.6},
abstract = {Deterministic graph grammars generate regular
graphs, that form a structural extension of
configuration graphs of pushdown systems. In this
paper, we study a probabilistic extension of regular
graphs obtained by labelling the terminal arcs of
the graph grammars by probabilities. Stochastic
properties of these graphs are expressed using PCTL,
a probabilistic extension of computation tree
logic. We present here an algorithm to perform
approximate verification of PCTL formulae. Moreover,
we prove that the exact model-checking problem for
PCTL on probabilistic regular graphs is undecidable,
unless restricting to qualitative properties. Our
results generalise those of [8], on probabilistic
pushdown automata, using similar methods combined
with graph grammars techniques.},
X-ID-HAL = {inria-00525388},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{ncma10,
author = {Morvan, C.},
title = {Contextual graph grammars characterising Rational
Graphs},
booktitle = {Non-Classical Models of Automata and Applications
(NCMA)},
pages = {141-153},
year = 2010,
address = {Jena, Germany},
month = {August},
abstract = {Deterministic graph grammars generate a family of
infinite graphs which characterise context- free
(word) languages. The present paper introduces a
context-sensitive extension of these gram- mars. We
prove that this extension characterises rational
graphs (whose traces are context- sensitive
languages). We illustrate that this extension is not
straightforward: the most obvious context-sensitive
graph rewriting systems generate non recursive
infinite graphs.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/ncma10.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00525409}
}
@InProceedings{ictss-a,
author = {Landry Nguena, O. and Marchand, H. and Rollet, A.},
title = {Automatic Test Generation for Data-Flow Reactive
Systems with time constraints (Short paper)},
booktitle = {22nd IFIP International Conference on Testing
Software and Systems},
year = 2010,
pages = {25-30},
address = {Natal, Brazil},
month = {November},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2010-ictss-short.pdf},
abstract = {In this paper, we handle the problem of conformance
testing for data-flow critical systems with time
constraints. We present a formal model (Variable
Driven Timed automata) adapted for such systems
inspired from timed automata using variables as
inputs and outputs, and clocks. In this model, we
consider urgency and the possibility to fire several
transitions instantaneously. We present a
conformance relation for this model and we propose a
test generation method using a test purpose
approach, based on a region graph transformation of
the specification.},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00530584}
}
@InProceedings{ictss-b,
author = {Falcone, Y. and Fernandez J.-C. and Jéron, T. and
Marchand, H. and Mounier, L.},
title = {More Testable Properties},
booktitle = {22nd IFIP International Conference on Testing
Software and Systems},
year = 2010,
address = {Natal, Brazil},
month = {November},
pages = {30-46},
volume = 6435,
publisher = {Springer},
series = {LNCS},
abstract = {In this paper, we explore the set of testable
properties within the Safety-Progress classification
where testability means to establish by testing that
a relation, between the tested system and the
property under scrutiny, holds. We characterize
testable properties wrt. several relations of
interest. For each relation, we give a sufficient
condition for a property to be testable. Then, we
study and delineate, for each Safety-Progress class,
the subset of testable properties and their
corresponding test oracle producing verdicts for the
possible test executions. Furthermore, we address
automatic test generation for the proposed
framework. Finally, we present a tool implementing
the results proposed by this paper.},
doi = {http://dx.doi.org/10.1007/978-3-642-16573-3_4},
pdf =
{http://www.irisa.fr/vertecs/Publis/Ps/2010-ICTSS.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00510018}
}
@TechReport{falcone10a,
author = {Falcone, Y. and Fernandez J.-C. and Jéron, T. and
Marchand, H. and Mounier, L.},
title = {More Testable Properties},
institution = {INRIA},
year = 2010,
type = {Research Report},
number = 7279,
month = {April},
abstract = {In this paper, we explore the set of testable
properties within the Safety-Progress classification
where testability means to establish by testing that
a relation, between the tested system and the
property under scrutiny, holds. We characterize
testable properties wrt. several relations of
interest. For each relation, we give a sufficient
condition for a property to be testable. Then, we
study and delineate, for each Safety-Progress class,
the subset of testable properties and their
corresponding test oracle producing verdicts for the
possible test executions. Furthermore, we address
automatic test generation for the proposed
framework. Finally, we present a tool implementing
the results proposed by this paper.},
pdf =
{http://hal.inria.fr/docs/00/48/42/97/PDF/RR-7279.pdf},
X-ID-HAL = {hal-00497350}
}
@InProceedings{wodes10-a,
author = {Darondeau, Ph. and Dubreil, J. and Marchand, H.},
title = {Supervisory Control for Modal Specifications of
Services},
booktitle = {Workshop on Discrete Event Systems, WODES'10},
pages = {428-435},
year = 2010,
address = {Berlin, Germany},
month = {August},
abstract = {In the service oriented architecture framework, a
modal specification, as defined by Larsen
in~\cite{Lar89}, formalises how a service should
interact with its environment. More precisely, a
modal specification determines the events that the
server may or must allow at each stage in an
interactive session. Therefore, techniques to
enforce a modal specification on a system would be
useful for practical applications. In this paper, we
investigate the adaptation of the supervisory
control theory of Ramadge and Wonham to enforce a
modal specification (with final states marking the
ends of the sessions) on a system modelled by a
finite LTS. We prove that there exists at most one
most permissive solution to this control problem. We
also prove that this solution is regular and we
present an algorithm for the effective computation
of the corresponding controller.},
URL-HAL = {http://hal.inria.fr/inria-00510013},
pdf =
{http://www.irisa.fr/vertecs/Publis/Ps/2010-Wodes-Modal.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00510013}
}
@TechReport{darondeau10a,
author = {Darondeau, Ph. and Dubreil, J. and Marchand, H.},
title = {Supervisory Control for Modal Specifications of
Services},
institution = {INRIA},
year = 2010,
type = {Research Report},
number = 7247,
month = {April},
abstract = {In the service oriented architecture framework, a
modal specification, as defined by Larsen
in~\cite{Lar89}, formalises how a service should
interact with its environment. More precisely, a
modal specification determines the events that the
server may or must allow at each stage in an
interactive session. Therefore, techniques to
enforce a modal specification on a system would be
useful for practical applications. In this paper, we
investigate the adaptation of the supervisory
control theory of Ramadge and Wonham to enforce a
modal specification (with final states marking the
ends of the sessions) on a system modelled by a
finite LTS. We prove that there exists at most one
most permissive solution to this control problem. We
also prove that this solution is regular and we
present an algorithm for the effective computation
of the corresponding controller.},
pdf =
{http://hal.inria.fr/docs/00/47/27/36/PDF/RR-7247.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00472736}
}
@Article{dubreil10,
author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.},
title = {Supervisory Control for Opacity},
journal = {IEEE Transactions on Automatic Control},
year = 2010,
volume = 55,
number = 5,
month = {May},
pages = {1089-1100},
doi = {http://dx.doi.org/10.1109/TAC.2010.2042008},
URL-HAL = {http://hal.inria.fr/inria-00483891},
abstract = { In the field of computer security, a problem that
received little attention so far is the enforcement
of confidentiality properties by supervisory
control. Given a critical system G that may leak
confidential information, the problem consists in
designing a controller C, possibly disabling
occurrences of a fixed subset of events of G, so
that the closed-loop system G/C does not leak
confidential information. We consider this problem
in the case where G is a finite transition system
with set of events A and an inquisitive user, called
the adversary, observes a subset A_a of A. The
confidential information is the fact (when it is
true) that the trace of the execution of G on A^*
belongs to a regular set S\subseteqA^*, called the
secret. The secret S is said to be opaque w.r.t. G
(resp. G/C) and A_a if the adversary cannot safely
infer this fact from the trace of the execution of G
(resp. G/C) on A_a^*. In the converse case, the
secret can be disclosed. We present an effective
algorithm for computing the most permissive
controller C such that S is opaque w.r.t. G/C and
A_a. This algorithm subsumes two earlier algorithms
working under the strong assumption that the
alphabet A_a of the adversary and the set of events
that the controller can disable are comparable.},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes},
X-ID-HAL = {inria-00483891}
}
@InProceedings{grr10,
author = {Gamatié, A. and Rusu, V. and Rutten, E.},
title = {Operational Semantics of the Marte Repetitive
Structure Modeling Concepts for Data-Parallel
Applications Design},
booktitle = {9th International Symposium on Parallel and
Distributed Computing (ISPDC'10)},
year = 2010,
month = {July},
pages = {25-32},
publisher = {IEEE Computer Society Press},
pdf =
{http://www.irisa.fr/vertecs/Publis/Ps/2010-ispdc.pdf},
doi = {http://dx.doi.org/10.1109/ISPDC.2010.30},
abstract = {This paper presents an operational semantics of the
repetitive model of computation, which is the basis
for the repetitive structure modeling (RSM) package
defined in the standard UML Marte profile. It also
deals with the semantics of an RSM extension for
control-oriented design. The goal of this semantics
is to serve as a formal support for i) reasoning
about the behavioral properties of models specified
in Marte with RSM, and ii) defining
correct-by-construction model transformations for
the production of executable code in a model-driven
engineering framework.},
x-international-audience ={yes},
x-proceedings ={yes},
X-ID-HAL = {inria-00522787}
}
@Article{gr10,
author = {Genet, Th. and Rusu, V.},
title = {Equational Approximations for Tree Automata
Completion},
journal = {Journal of Symbolic Computation},
year = 2010,
volume = 45,
number = 5,
pages = {574-597},
month = {May},
doi = {http://dx.doi.org/10.1016/j.jsc.2010.01.009},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/rusu2010.pdf},
abstract = {In this paper we deal with the verification of
safety properties of infinite-state systems modeled
by term rewriting systems. An over-approximation of
the set of reachable terms of a term rewriting
system image is obtained by automatically
constructing a finite tree automaton. The
construction is parameterized by a set E of
equations on terms, and we also show that the
approximating automata recognize at most the set of
image-reachable terms. Finally, we present some
experiments carried out with the implementation of
our algorithm. In particular, we show how some
approximations from the literature can be defined
using equational approximations.},
X-ID-HAL = {inria-00495405},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes}
}
@InProceedings{delaval10a,
author = {Delaval, G. and Marchand, H. and Rutten, E.},
title = {Contracts for Modular Discrete Controller Synthesis},
booktitle = {Conference on Languages, Compilers and Tools for
Embedded Systems, LCTES 2010},
pages = {57-66},
year = 2010,
doi = {http://dx.doi.org/10.1145/1755888.1755898},
pdf =
{http://www.irisa.fr/vertecs/Publis/Ps/2010-LCTES.pdf},
abstract = {We describe the extension of a reactive programming
language with a behavioral contract construct. It is
dedicated to the pro- gramming of reactive control
of applications in embedded sys- tems, and involves
principles of the supervisory control of discrete
event systems. Our contribution is in a language
approach where modular discrete controller synthesis
(DCS) is integrated, and it is concretized in the
encapsulation of DCS into a compilation pro-
cess. From transition system specifications of
possible behaviors, DCS automatically produces
controllers that make the controlled system satisfy
the property given as objective. Our language fea-
tures and compiling technique provide
correctness-by-construction in that sense, and
enhance reliability and verifiability. Our appli-
cation domain is adaptive and reconfigurable
systems: closed-loop adaptation mechanisms enable
flexible execution of functionalities
w.r.t. changing resource and environment
conditions. Our language can serve programming such
adaption controllers. This paper par- ticularly
describes the compilation of the language. We
present a method for the modular application of
discrete controller synthesis on synchronous
programs, and its integration in the BZR
language. We consider structured programs, as a
composition of nodes, and first apply DCS on
particular nodes of the program, in order to re-
duce the complexity of the controller computation;
then, we allow the abstraction of parts of the
program for this computation; and finally, we show
how to recompose the different controllers com-
puted from different abstractions for their correct
co-execution with the initial program. Our work is
illustrated with examples, and we present
quantitative results about its implementation.},
address = {Stockholm, Sweden},
X-ID-HAL = {inria-00476910},
month = {April},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{wodes10-b,
author = {Dumitrescu, E. and Girault, A. and Marchand, H. and
Rutten, E.},
title = {Multicriteria optimal discrete controller synthesis
for fault-tolerant real-time tasks},
booktitle = {Workshop on Discrete Event Systems, WODES'10},
pages = {366-373},
year = 2010,
address = {Berlin, Germany},
month = {August},
abstract = {We propose a technique for discrete controller
synthesis, with optimal synthesis on bounded paths,
in order to model, design, and optimize
fault-tolerant distributed systems, taking into
account several criteria (e.g., the execution costs
of the tasks and their quality of service).
Different combinations are explored for
multi-criteria optimization.},
pdf =
{http://www.irisa.fr/vertecs/Publis/Ps/2010-Wodes-Fault-tolerant.pdf},
X-ID-HAL = {inria-00510019},
x-international-audience ={yes},
x-proceedings ={yes}
}