\n \n \n
\n
\n\n \n \n \n \n \n \n Dynamic Observers for the Synthesis of Opaque Systems.\n \n \n \n \n\n\n \n Cassez, F.; Dubreil, J.; and Marchand, H.\n\n\n \n\n\n\n In Liu, Z.; and Ravn, A. P., editor(s),
Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799, of
Lecture Notes in Computer Science, pages 352–367, 2009. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
Slides\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atva/CassezDM09,\n author = {Franck Cassez and\n J{\\'{e}}r{\\'{e}}my Dubreil and\n Herv{\\'{e}} Marchand},\n editor = {Zhiming Liu and\n Anders P. Ravn},\n title = {Dynamic Observers for the Synthesis of Opaque Systems},\n booktitle = {Automated Technology for Verification and Analysis, 7th International\n Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},\n pages = {352--367},\n year = {2009},\n series = {Lecture Notes in Computer Science},\n volume = {5799},\n publisher = {Springer},\n url = {http://dx.doi.org/10.1007/978-3-642-04761-9_26},\n doi = {10.1007/978-3-642-04761-9_26},\n urlpaper = {papers/atva-09.pdf},\n urlslides = {papers/slides-atva-09.pdf},\n Type = {B - International Conferences},\n\n ABSTRACT = { In this paper, we address the problem of synthesizing \\emph{opaque}\n systems by selecting the set of observable\n events.\n We first investigate the case of \\emph{static} observability\n where the set of observable events\n is fixed a priori. In this context, we show that checking whether a\n system is opaque and computing an optimal static observer ensuring\n opacity are both PSPACE-complete problems.\n Next, we introduce \\emph{dynamic} partial observability where the\n set of observable events\n can\n change over time.\n We show how to check that a system is opaque \\wrt a dynamic observer\n and also address the corresponding synthesis problem: given a system\n $G$ and secret states $S$, compute the set of dynamic observers\n under which $S$ is opaque. Our main result is that the synthesis\n problem can be solved in EXPTIME.},\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper, we address the problem of synthesizing \\emphopaque systems by selecting the set of observable events. We first investigate the case of \\emphstatic observability where the set of observable events is fixed a priori. In this context, we show that checking whether a system is opaque and computing an optimal static observer ensuring opacity are both PSPACE-complete problems. Next, we introduce \\emphdynamic partial observability where the set of observable events can change over time. We show how to check that a system is opaque ≀t a dynamic observer and also address the corresponding synthesis problem: given a system $G$ and secret states $S$, compute the set of dynamic observers under which $S$ is opaque. Our main result is that the synthesis problem can be solved in EXPTIME.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n A note on fault diagnosis algorithms.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In Ouaknine, J.; and Vaandrager, F. W., editor(s),
Proceedings of the 48th IEEE Conference on Decision and Control, CDC 2009, combined withe the 28th Chinese Control Conference, December 16-18, 2009, Shanghai, China, pages 6941–6946, 2009. IEEE\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
Slides\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cdc/Cassez09,\n author = {Franck Cassez},\n title = {A note on fault diagnosis algorithms},\n booktitle = {Proceedings of the 48th {IEEE} Conference on Decision and Control,\n {CDC} 2009, combined withe the 28th Chinese Control Conference, December\n 16-18, 2009, Shanghai, China},\n editor = {Jo{\\"{e}}l Ouaknine and\n Frits W. Vaandrager},\n pages = {6941--6946},\n year = {2009},\n publisher = {{IEEE}},\n year = {2009},\n url = {http://dx.doi.org/10.1109/CDC.2009.5399968},\n doi = {10.1109/CDC.2009.5399968},\n ABSTRACT = { In this paper we review algorithms for checking diagnosability of\n discrete-event systems and timed automata. We point out that the\n diagnosability problems in both cases reduce to the emptiness\n problem for (timed) B\\"uchi automata. Moreover, it is known that,\n checking whether a discrete-event system is diagnosable, can also be\n reduced to checking bounded diagnosability. We establish a similar\n result for timed automata. We also provide a synthesis of the\n complexity results for the different fault diagnosis problems.},\n urlpaper = {papers/cdc-09.pdf},\n urlslides = {papers/slides-cdc-09.pdf},\n Type = {B - International Conferences},\n\n keywords = {diagnosis, timed automata},\n}\n\n\n\n
\n
\n\n\n
\n In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to the emptiness problem for (timed) Büchi automata. Moreover, it is known that, checking whether a discrete-event system is diagnosable, can also be reduced to checking bounded diagnosability. We establish a similar result for timed automata. We also provide a synthesis of the complexity results for the different fault diagnosis problems.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Synthesis of Non-Interferent Timed Systems.\n \n \n \n \n\n\n \n Benattar, G.; Cassez, F.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n In
Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813, of
Lecture Notes in Computer Science, pages 28–42, 2009. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
Slides\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/formats/BenattarCLR09,\n author = {Gilles Benattar and\n Franck Cassez and\n Didier Lime and\n Olivier H. Roux},\n title = {Synthesis of Non-Interferent Timed Systems},\n booktitle = {Formal Modeling and Analysis of Timed Systems, 7th International Conference,\n {FORMATS} 2009, Budapest, Hungary, September 14-16, 2009. Proceedings},\n pages = {28--42},\n year = {2009},\n series = {Lecture Notes in Computer Science},\n volume = {5813},\n publisher = {Springer},\n url = {http://dx.doi.org/10.1007/978-3-642-04368-0_5},\n doi = {10.1007/978-3-642-04368-0_5},\n urlpaper = {papers/formats-09.pdf},\n urlslides = {papers/slides-formats-09.pdf},\n ABSTRACT = { In this paper, we focus on the synthesis of secure timed systems\n which are given by timed automata.\n The security property that the system must satisfy is a\n \\emph{non-interference} property.\n Various notions of non-interference have been defined in the\n literature, and in this paper we focus on \\emph{Strong\n Non-deterministic Non-Interference} (SNNI)\n and we study the two following problems: ($1$) check whether it is\n possible to enforce a system to be SNNI; if yes ($2$) compute a\n sub-system which is SNNI.},\n Type = {B - International Conferences},\n\n keywords = {security, timed automata}\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a \\emphnon-interference property. Various notions of non-interference have been defined in the literature, and in this paper we focus on \\emphStrong Non-deterministic Non-Interference (SNNI) and we study the two following problems: ($1$) check whether it is possible to enforce a system to be SNNI; if yes ($2$) compute a sub-system which is SNNI.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study.\n \n \n \n \n\n\n \n Cassez, F.; Jessen, J. J.; Larsen, K. G.; Raskin, J.; and Reynier, P.\n\n\n \n\n\n\n In Majumdar, R.; and Tabuada, P., editor(s),
Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings, volume 5469, of
Lecture Notes in Computer Science, pages 90–104, 2009. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/hybrid/CassezJLRR09,\n author = {Franck Cassez and\n Jan Jakob Jessen and\n Kim Guldstrand Larsen and\n Jean{-}Fran{\\c{c}}ois Raskin and\n Pierre{-}Alain Reynier},\n editor = {Rupak Majumdar and\n Paulo Tabuada},\n title = {Automatic Synthesis of Robust and Optimal Controllers - An Industrial\n Case Study},\n booktitle = {Hybrid Systems: Computation and Control, 12th International Conference,\n {HSCC} 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings},\n pages = {90--104},\n year = {2009},\n crossref = {DBLP:conf/hybrid/2009},\n url = {http://dx.doi.org/10.1007/978-3-642-00602-9_7},\n series = {Lecture Notes in Computer Science},\n volume = {5469},\n publisher = {Springer},\n doi = {10.1007/978-3-642-00602-9_7},\n urlpaper = {papers/hscc-09.pdf},\n keywords = {control, synthesis, hybrid automata},\n Type = {B - International Conferences},\n\n abstract = { Int his paper,we show how to apply recent tools for the automatic synthesis of robust and near-optimal controllers for a real industrial case study. We show how to use three different classes of models and their supporting existing tools, UPPAAL-TIGA for synthesis, PHAVER for verification, and SIMULINK for simulation, in a complementary way. We believe that this case study shows that our tools have reached a level of maturity that allows us to tackle interesting and relevant industrial control problems.}\n }\n\n\n\n\n
\n
\n\n\n
\n Int his paper,we show how to apply recent tools for the automatic synthesis of robust and near-optimal controllers for a real industrial case study. We show how to use three different classes of models and their supporting existing tools, UPPAAL-TIGA for synthesis, PHAVER for verification, and SIMULINK for simulation, in a complementary way. We believe that this case study shows that our tools have reached a level of maturity that allows us to tackle interesting and relevant industrial control problems.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n The Dark Side of Timed Opacity.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In Park, J. H.; Chen, H.; Atiquzzaman, M.; Lee, C.; Kim, T.; and Yeo, S., editor(s),
Advances in Information Security and Assurance, Third International Conference and Workshops, ISA 2009, Seoul, Korea, June 25-27, 2009. Proceedings, volume 5576, of
Lecture Notes in Computer Science, pages 21–30, 2009. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
Slides\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sersc-isa/Cassez09,\n author = {Franck Cassez},\n title = {The Dark Side of Timed Opacity},\n editor = {Jong Hyuk Park and\n Hsiao{-}Hwa Chen and\n Mohammed Atiquzzaman and\n Changhoon Lee and\n Tai{-}Hoon Kim and\n Sang{-}Soo Yeo},\n booktitle = {Advances in Information Security and Assurance, Third International\n Conference and Workshops, {ISA} 2009, Seoul, Korea, June 25-27, 2009.\n Proceedings},\n series = {Lecture Notes in Computer Science},\n volume = {5576},\n publisher = {Springer},\n pages = {21--30},\n year = {2009},\n crossref = {DBLP:conf/sersc-isa/2009},\n urlpaper = {papers/isa-09.pdf},\n urlslides = {papers/slides-isa-09.pdf},\n Type = {B - International Conferences},\n\n doi = {10.1007/978-3-642-02617-1_3},\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Communicating Embedded Systems.\n \n \n \n \n\n\n \n Cassez, F.; and Markey, N.\n\n\n \n\n\n\n Communicating Embedded Systems, pages 83–120. Jard, C.; and Roux, O. H., editor(s). ISTE Ltd. – John Wiley & Sons, Ltd, October 2009.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inbook{cassez-control-iste-2009,\n author = {Franck Cassez and Markey, Nicolas},\n title = {Communicating Embedded Systems},\n editor = {Jard, Claude and Roux, Olivier H.},\n month = oct,\n pages = {83--120},\n publisher = {ISTE Ltd. -- John Wiley \\& Sons, Ltd},\n chapter = {Control of Timed Systems},\n xxurl = {http://www.iste.co.uk/index.php?ACTION=Browse&CatParent=FUB2},\n year = {2009},\n urlpaper = {papers/iste-wiley-book-control.pdf},\nabstract={In this book Chapter we address the problem of controller synthesis for timed systems. By\ntimed systems we refer to systems which are subject to quantitative (hard) real-time\nconstraints. We assume the reader is familiar with the basics of Timed Automata\ntheory, or has read Chapter 1 and Chapter 2 in this book. },\nXXnote={Draft version may differ from published one.},\n Type = {C - Book Chapters},\n\n}\n\n\n\n
\n
\n\n\n
\n In this book Chapter we address the problem of controller synthesis for timed systems. By timed systems we refer to systems which are subject to quantitative (hard) real-time constraints. We assume the reader is familiar with the basics of Timed Automata theory, or has read Chapter 1 and Chapter 2 in this book. \n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Communicating Embedded Systems.\n \n \n \n \n\n\n \n Cassez, F.; and Tripakis, S.\n\n\n \n\n\n\n Communicating Embedded Systems, pages 120–151. Jard, C.; and Roux, O. H., editor(s). ISTE Ltd. – John Wiley & Sons, Ltd, October 2009.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inbook{cassez-diag-iste-2009,\n author = {Franck Cassez and Tripakis, Stavros},\n title = {Communicating Embedded Systems},\n editor = {Jard, Claude and Roux, Olivier H.},\n month = oct,\n pages = {120--151},\n publisher = {ISTE Ltd. -- John Wiley \\& Sons, Ltd},\n chapter = {Fault Diagnosis of Timed Systems},\n xxurl = {http://www.iste.co.uk/index.php?ACTION=Browse&CatParent=FUB2},\n year = {2009},\n Type = {C - Book Chapters},\n\n urlpaper = {papers/iste-wiley-book-diag.pdf},\nabstract={In this book Chapter, we review the main results pertaining\n to the problem of fault diagnosis of timed\n automata. Timed automata are introduced in Chapter 1\n and Chapter 2 in this book, and the reader not\n familiar with this model is invited to read them\n first.},\nXXnote={Draft version may differ from published one.}\n}\n\n\n\n
\n
\n\n\n
\n In this book Chapter, we review the main results pertaining to the problem of fault diagnosis of timed automata. Timed automata are introduced in Chapter 1 and Chapter 2 in this book, and the reader not familiar with this model is invited to read them first.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n How to Install PHAVer on Mac OS X.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n Short Note, NICTA, Sydney, Australia, 2009.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
link\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@MISC{cassez-compile-phaver-09,\n AUTHOR = {Franck Cassez},\n HOWPUBLISHED = {Short Note, NICTA, Sydney, Australia},\n KEYWORDS = {PHAVer, OS X},\n TITLE = {{How to Install PHAVer on Mac OS X}},\n urlpaper = {papers/install-phaver-09.pdf},\n YEAR = {2009},\nURL_link={http://www-verimag.imag.fr/~frehse/phaver_web/index.html},\nabstract={This short note explains how to install PHAVer (and the\n needed libraries) for a single user on Mac OS X\n running Leopard (10.5.6). It might also work for\n earlier versions (you can report to me in case of a\n successful install on earlier version).},\n Type = {E - Reports},\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2008\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n This short note explains how to install PHAVer (and the needed libraries) for a single user on Mac OS X running Leopard (10.5.6). It might also work for earlier versions (you can report to me in case of a successful install on earlier version).\n
\n\n\n
\n\n\n\n\n\n