L'analyse des systèmes communiquant par file a fait l'objet d'études scientifiques nombreuses mais qui n'ont pu offrir des solutions totalement satisfaisantes. Nous proposons d'aborder ce problème dans le cadre de l'interprétation abstraite, en définissant des treillis abstraits adaptés à ce type de systèmes. Nous considérons d'abord le cas où les messages échangés sont assimilables à un alphabet fini, puis nous nous attaquons au cas, plus difficile, des messages portant des valeurs entières ou réelles. Ce problème nous amène à définir et à étudier un nouveau type d'automate, les automates de treillis. Ces automates de treillis peuvent également être utilisés pour l'analyses des programmes utilisant une pile d'appels.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/LeGall.pdf} } @inproceedings{BBBM-qest08, author = {Bertrand, N. and Bouyer, P. and Brihaye, Th. and Markey, N.}, title = {Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics}, pages = {55-64}, address = {Saint Malo, France}, booktitle = {Proceedings of the 5th International Conference on the Quantitative Evaluation of SysTems (QEST'08)}, month = septembre, publisher = {IEEE Computer Society Press}, year = 2008, doi = {http://dx.doi.org/10.1109/QEST.2008.19}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/BBBM-qest08.pdf}, abstract = {In a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of single-clock timed automata. In this paper, we consider the quantitative model-checking problem for omega-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an omega-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm,and finally prove that we can decide the threshold problem in that framework. }, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {BE} } @InProceedings{opacity2, author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.}, title = {Opacity Enforcing Control Synthesis}, booktitle = {Workshop on Discrete Event Systems, WODES'08}, address = {Gothenburg, Sweden}, month = mars, year = 2008, pages = {28-35}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2008-Wodes-Opacity.pdf}, abstract = {Given a finite transition system and a regular predicate, we address the problem of computing a controller enforcing the opacity of the predicate against an attacker (who partially observes the system), supposedly trying to push the system to reveal the predicate. Assuming that the controller can only control a subset of the events it observes (possibly different from the ones of the attacker), we show that an optimal control always exists and provide sufficient conditions under which it is regular and effectively computable. These conditions rely on the inclusion relationships between the controllable alphabet and the observable alphabets of the attacker and of the controller. }, x-international-audience ={yes}, x-proceedings ={yes} } @InBook{book-chap-react-systems, Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.}, editor = { Merz, S. and Navet, N.}, Title = {Validation of Reactive Systems}, BookTitle = {Modeling and Verification of Real-TIME Systems -- Formalisms and software Tools}, Chapter = 2, Publisher = {Hermès Science}, Year = 2008, Pages = {51-76}, month = janvier, x-editorial-board ={yes} } @article{komenda-automatica, author = {Komenda, J. and van Schuppen, J. and Gaudin, B. and Marchand, H.}, title = {Supervisory Control of Modular Systems with Global Specification Languages}, journal = {Automatica}, year = 2008, volume = 44, number = 4, month = avril, pages = {1127--1134}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2008-Automatica.pdf}, doi = {http://dx.doi.org/10.1016/j.automatica.2007.09.004}, abstract = {The paper presents sufficient conditions for modular (supervisory) control synthesis to equal global control synthesis. In modular control synthesis a supervisory control is synthesized for each module separately and the supervisory control consists of the parallel composition of the modular supervisory controls. The general case of the specification that is indecomposable and not necessarily contained in the plant language, which is often the case in practice, is considered. The usual assumption that all shared events are controllable is relaxed by introducing two new structural conditions relying on the global mutual controllability condition. The novel concept used as a sufficient structural condition is strong global mutual controllability. The main result uses a weaker condition called global mutual controllability together with local consistency of the specification. An example illustrates the approach.}, x-international-audience ={yes}, x-proceedings ={yes}, x-editorial-board ={yes}, x-pays = {CZ,NL} } @inproceedings{BBBBG-lics08, address = {Pittsburgh, PA, USA}, author = {Baier, Ch. and Bertrand, N. and Bouyer, P. and Brihaye, Th. and Groesser, M.}, booktitle = {{P}roceedings of the 23rd {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'08)}, pages = {217-226}, month = juin, publisher = {IEEE Computer Society Press}, title = {Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata}, year = 2008, abstract = {In this paper, we define two relaxed semantics (one based on probabilities and the other one based on the topological notion of largeness) for LTL over infinite runs of timed automata which rule out unlikely sequences of events. We prove that these two semantics match in the framework of single-clock timed automata (and only in that framework), and prove that the corresponding relaxed model-checking problems are PSPACE-Complete. Moreover, we prove that the probabilistic non-Zenoness can be decided for single-clock timed automata in NLOGSPACE.}, doi = {http://dx.doi.org/10.1109/LICS.2008.25}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/BBBBG-lics08.pdf}, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {DE} } @inproceedings{BBG-fossacs08, address = {Budapest, Hungary}, author = {Baier, Ch. and Bertrand, N. and Groesser, M.}, booktitle = {Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08)}, month = mars, publisher = {Springer}, series = {LNCS}, volume = {4962}, pages = {287-301}, title = {On Decision Problems for Probabilistic Büchi Automata}, year = 2008, abstract = {Probabilistic Büchi automata (PBA) are finite-state acceptors for infinite words where all choices are resolved by fixed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. The main contribution of this paper is a complementation operator for PBA and a discussion on several algorithmic problems for PBA. All interesting problems, such as checking emptiness or equivalence for PBA or checking whether a finite transition system satisfies a PBA-specification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partially-observable Markov decision processes and omega-regular winning objectives. Furthermore, we discuss an alternative semantics for PBA where it is required that almost all runs for an accepted word are accepting, which turns out to be less powerful, but has a decidable emptiness problem.}, pdf = {http://www.irisa.fr/prive/nbertran/BBG-fossacs08.pdf}, doi = {http://dx.doi.org/10.1007/978-3-540-78499-9_21}, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {DE} } @InProceedings{ifac2008, author = {J\'eron, T. and Marchand, H. and Genc, S. and Lafortune, S.}, title = {Predictability of Sequence Patterns in Discrete Event Systems}, booktitle = {IFAC World Congress}, year = 2008, address = {Seoul, Korea}, month = juillet, pages = {537-453}, abstract = {The problem of predicting the occurrences of a pattern in a partially-observed discrete-event system is studied. The system is modeled by a labeled transition system. The pattern is a set of event sequences modeled by a finite-state automaton. The occurrences of the pattern are predictable if it is possible to infer about any occurrence of the pattern before the pattern is completely executed by the system. An off-line algorithm to verify the property of predictability is presented. The verification is polynomial in the number of states of the system. An on-line algorithm to track the execution of the pattern during the operation of the system is also presented. This algorithm is based on the use of a diagnoser automaton. The results are illustrated using an example from computer systems.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2008-IFAC-Predictability.pdf}, x-international-audience ={yes}, x-proceedings ={yes} } @TECHREPORT{opacity, author = {Dubreil, J. and Jéron, T. and Marchand, H.}, title = {Monitoring Information flow by Diagnosis Techniques}, institution = {IRISA}, year = 2008, number = 1901, month = aout, abstract = {In this paper, we are interested in constructing monitors for the detection of confidential information flow in the context of partially observable discrete event systems. We focus on the case where the secret information is given as a regular language. We first characterize the set of observations allowing an attacker to infer the secret behaviors. We consider the general case where the attacker and the administrator have different partial views of the system. Further, based on the diagnosis of discrete event systems, we provide necessary and sufficient conditions under which detection and prediction of secret information flow can be ensured and a construction of a monitor ensuring this task.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2008-PI-1901-Detec-Opacity.pdf} } @TECHREPORT{PI-opacity, author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.}, title = {Opacity Enforcing Control Synthesis}, institution = {IRISA}, year = 2008, number = 1887, month = mars, abstract = {Given a finite transition system and a regular predicate, we address the problem of computing a controller enforcing the opacity of the predicate against an attacker (who partially observes the system), supposedly trying to push the system to reveal the predicate. Assuming that the controller can only control a subset of the events it observes (possibly different from the ones of the attacker), we show that an optimal control always exists and provide sufficient conditions under which it is regular and effectively computable. These conditions rely on the inclusion relationships between the controllable alphabet and the observable alphabets of the attacker and of the controller}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/PI-Opacity.pdf} } @Misc{politess-1, author = {Marchand, H. and Dubreil, J. and Jéron, T.}, title = {Automatic Test Generation for Security Property}, howpublished = {Delivrable, Politess Project}, year = 2008 } @Misc{politess-2, author = {Hélouët, L. and Marchand, H. and Jéron, T.}, title = {Testing Cover Channel}, howpublished = {Delivrable, Politess Project}, year = 2008 } @Misc{politess-3, author = {Dubreil, J. and Jéron, T. and Hélouët, L. and Marchand, H.}, title = {Evaluation des techniques de diagnostic pour la construction de détecteurs d'intrusions}, howpublished = {Delivrable, Politess Project}, year = 2008 } @Misc{, }