%% 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} }