var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https://franck44.github.io/publications/franck-pubs.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https://franck44.github.io/publications/franck-pubs.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https://franck44.github.io/publications/franck-pubs.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formal and Executable Semantics of the EVM in Dafny.\n \n \n \n \n\n\n \n Cassez, F.; Fuller, J.; Ketabi, M.; Pearce, D.; and Quiles, H. M. A.\n\n\n \n\n\n\n In International Symposium on Formal Methods (FM'23), of Lecture Notes in Computer Science, 2023. Springer\n Forthcoming.\n\n\n\n
\n\n\n\n \n \n \"FormalXx\n  \n \n \n \"FormalPaper\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 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{dafnyevm-fm-23,\n  author    = {Franck Cassez and\n               Joanne Fuller and Milad Ketabi and David Pearce and \n               Horacio Mijail Anton Quiles},\n  title     = {Formal and Executable Semantics of the EVM in Dafny},\n  booktitle = {International Symposium on Formal Methods (FM'23)},\n  xxpages     = {445-462},\n  year      = {2023},\n  series    = {Lecture Notes in Computer Science},\n  xxxvolume    = {13047},\n  publisher = {Springer},  \n  note        = {Forthcoming.},\n  urlxx       = {},\n  xxxdoi       = {http://doi.org/10.1007/978-3-030-90870-6 24},\n\n  urlpaper = {papers/dafnyevm-fm-23.pdf},\n  abstract = {The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.}\n}\n\n
\n
\n\n\n
\n The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Deductive Verification of Smart Contracts with Dafny.\n \n \n \n \n\n\n \n Cassez, F.; Fuller, J.; and Quiles, H. M. A.\n\n\n \n\n\n\n In Groote, J. F.; and Huisman, M., editor(s), Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, Proceedings, volume 13487, of Lecture Notes in Computer Science, pages 50–66, 2022. Springer\n FMICS Best Paper Award\n\n\n\n
\n\n\n\n \n \n \"DeductivePaper\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 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fmics/CassezFQ22,\n  author    = {Franck Cassez and\n               Joanne Fuller and\n               Horacio Mijail Anton Quiles},\n  editor    = {Jan Friso Groote and\n               Marieke Huisman},\n  title     = {Deductive Verification of Smart Contracts with Dafny},\n  booktitle = {Formal Methods for Industrial Critical Systems - 27th International\n               Conference, {FMICS} 2022, Warsaw, Poland, September 14-15, 2022, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13487},\n  pages     = {50--66},\n  publisher = {Springer},\n  year      = {2022},\n  url       = {https://doi.org/10.1007/978-3-031-15008-1\\_5},\n  doi       = {10.1007/978-3-031-15008-1\\_5},\n  timestamp = {Sat, 10 Sep 2022 20:58:36 +0200},\n  biburl    = {https://dblp.org/rec/conf/fmics/CassezFQ22.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note            = {FMICS Best Paper Award},\n  abstract = {\n    We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.\n  }\n}\n\n
\n
\n\n\n
\n We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Deductive Verification of Smart Contracts with Dafny.\n \n \n \n \n\n\n \n Cassez, F.; Fuller, J.; and Quiles, H. M. A.\n\n\n \n\n\n\n CoRR, abs/2208.02920. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"DeductivePaper\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 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-2208-02920,\n  author    = {Franck Cassez and\n               Joanne Fuller and\n               Horacio Mijail Anton Quiles},\n  title     = {Deductive Verification of Smart Contracts with Dafny},\n  journal   = {CoRR},\n  volume    = {abs/2208.02920},\n  year      = {2022},\n  url       = {https://doi.org/10.48550/arXiv.2208.02920},\n  doi       = {10.48550/arXiv.2208.02920},\n  eprinttype = {arXiv},\n  eprint    = {2208.02920},\n  timestamp = {Wed, 10 Aug 2022 14:49:54 +0200},\n  biburl    = {https://dblp.org/rec/journals/corr/abs-2208-02920.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  abstract = {We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.}\n}\n\n\n
\n
\n\n\n
\n We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of the Ethereum 2.0 Beacon Chain.\n \n \n \n \n\n\n \n Cassez, F.; Fuller, J.; and Asgaonkar, A.\n\n\n \n\n\n\n In Fisman, D.; and Rosu, G., editor(s), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243, of Lecture Notes in Computer Science, pages 167–182, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\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 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tacas/CassezFA22,\n  author    = {Franck Cassez and\n               Joanne Fuller and\n               Aditya Asgaonkar},\n  editor    = {Dana Fisman and\n               Grigore Rosu},\n  title     = {Formal Verification of the Ethereum 2.0 Beacon Chain},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n               - 28th International Conference, {TACAS} 2022, Held as Part of the\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\n               2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13243},\n  pages     = {167--182},\n  publisher = {Springer},\n  year      = {2022},\n  url       = {https://doi.org/10.1007/978-3-030-99524-9\\_9},\n  doi       = {10.1007/978-3-030-99524-9\\_9},\n  timestamp = {Fri, 29 Apr 2022 14:50:36 +0200},\n  biburl    = {https://dblp.org/rec/conf/tacas/CassezFA22.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  urlpaper = {papers/eth2-tacas-22.pdf},\n  abstract = {We report our experience in the formal verification of the reference implementation of the Beacon Chain.\n  The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking \n  information about the validators,\n  their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes).   \n  The Beacon Chain is mission-critical and any bug in it could compromise the whole  network.\n  The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. \n  We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny.\n  During the course of this work, we have uncovered several issues, proposed verified fixes.\n  We have also synthesised functional correctness specifications that enable us to provide guarantees beyond\n  runtime errors. Our software artefact with the code and proofs in Dafny is available at \\url{https://github.com/ConsenSys/eth2.0-dafny}.}\n}\n\n
\n
\n\n\n
\n We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at ˘rlhttps://github.com/ConsenSys/eth2.0-dafny.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verification of the Incremental Merkle Tree Algorithm with Dafny.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In International Symposium on Formal Methods (FM'21), volume 13047, of Lecture Notes in Computer Science, pages 445-462, 2021. Springer\n \n\n\n\n
\n\n\n\n \n \n \"VerificationXx\n  \n \n \n \"VerificationPaper\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 13 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{merkle-fm-21,\n  author    = {Franck Cassez},\n  title     = {Verification of the Incremental Merkle Tree Algorithm with Dafny},\n  booktitle = {International Symposium on Formal Methods (FM'21)},\n  pages     = {445-462},\n  year      = {2021},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13047},\n  publisher = {Springer},  \n  xxxnote        = {Forthcoming.},\n  urlxx       = {},\n  doi       = {http://doi.org/10.1007/978-3-030-90870-6 24},\n\n  urlpaper = {papers/merkle-fm-21.pdf},\n  abstract = {The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.}\n}\n\n
\n
\n\n\n
\n The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of the Ethereum 2.0 Beacon Chain.\n \n \n \n \n\n\n \n Cassez, F.; Fuller, J.; and Asgaonkar, A.\n\n\n \n\n\n\n CoRR, abs/2110.12909. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \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
@article{DBLP:journals/corr/abs-2110-12909,\n  author    = {Franck Cassez and\n               Joanne Fuller and\n               Aditya Asgaonkar},\n  title     = {Formal Verification of the Ethereum 2.0 Beacon Chain},\n  journal   = {CoRR},\n  volume    = {abs/2110.12909},\n  year      = {2021},\n  url       = {https://arxiv.org/abs/2110.12909},\n  eprinttype = {arXiv},\n  eprint    = {2110.12909},\n  timestamp = {Thu, 28 Oct 2021 15:25:31 +0200},\n  biburl    = {https://dblp.org/rec/journals/corr/abs-2110-12909.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verification of the Incremental Merkle Tree Algorithm with Dafny.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n CoRR, abs/2105.06009. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\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 13 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-2021,\n    title={Verification of the Incremental Merkle Tree Algorithm with Dafny}, \n    author={Franck Cassez},\n    year={2021},\n    eprint={2105.06009},\n    archivePrefix={arXiv},\n    primaryClass={cs.LO},\n    abstract={\n    The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.\n    },\n  journal   = {CoRR},\n  volume    = {abs/2105.06009},\n  url       = {https://arxiv.org/abs/2105.06009}\n}\n  \n
\n
\n\n\n
\n The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction.\n \n \n \n \n\n\n \n Cassez, F.; Jensen, P. G.; and Larsen, K. G.\n\n\n \n\n\n\n Fundam. Informaticae, 178(1-2): 31–57. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\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 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/fuin/CassezJL21,\n  author    = {Franck Cassez and\n               Peter Gj{\\o}l Jensen and\n               Kim Guldstrand Larsen},\n  title     = {Verification and Parameter Synthesis for Real-Time Programs using\n               Refinement of Trace Abstraction},\n  journal   = {Fundam. Informaticae},\n  abstract = {We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. \nWe propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. \nAll of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.},\n\n  volume    = {178},\n  number    = {1-2},\n  pages     = {31--57},\n  year      = {2021},\n  url       = {https://doi.org/10.3233/FI-2021-1997},\n  doi       = {10.3233/FI-2021-1997},\n  timestamp = {Fri, 22 Jan 2021 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/journals/fuin/CassezJL21.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n   urlpaper = {papers/fi-2021.pdf},\n}\n\n
\n
\n\n\n
\n We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction.\n \n \n \n \n\n\n \n Cassez, F.; Jensen, P. G.; and Larsen, K. G.\n\n\n \n\n\n\n CoRR, abs/2007.10539. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\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 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-2007-10539,\n  author    = {Franck Cassez and\n               Peter Gj{\\o}l Jensen and\n               Kim Guldstrand Larsen},\n  title     = {Verification and Parameter Synthesis for Real-Time Programs using\n               Refinement of Trace Abstraction},\n  journal   = {CoRR},\n  abstract = {We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. \nWe propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. \nAll of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.},\n  volume    = {abs/2007.10539},\n  year      = {2020},\n  url       = {https://arxiv.org/abs/2007.10539},\n  archivePrefix = {arXiv},\n  eprint    = {2007.10539},\n  timestamp = {Tue, 28 Jul 2020 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/journals/corr/abs-2007-10539.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n
\n We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Efficient and Scalable Runtime Monitoring for Cyber-Physical System.\n \n \n \n \n\n\n \n Zheng, X.; Julien, C.; Podorozhny, R. M.; Cassez, F.; and Rakotoarivelo, T.\n\n\n \n\n\n\n IEEE Syst. J., 12(2): 1667–1678. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/sj/Zheng0PCR18,\n  author    = {Xi Zheng and\n               Christine Julien and\n               Rodion M. Podorozhny and\n               Franck Cassez and\n               Thierry Rakotoarivelo},\n  title     = {Efficient and Scalable Runtime Monitoring for Cyber-Physical System},\n  journal   = {{IEEE} Syst. J.},\n  abstract={\n  Our reliance on cyber-physical systems (CPSs) is increasingly widespread, but scalable methods for the analysis of such systems remain a significant challenge. Runtime verification of CPSs provides a reasonable middle ground between formal verification and simulation approaches, but it comes with its own challenges. A runtime verification system must run directly on the deployed application. In the CPS domain, it is therefore critical that a runtime verification system exhibits low overhead and good scalability so that the verification does not interfere with the analyzed CPS application. In this paper, we introduce Brace, a runtime verification system whose focus is on ensuring these performance qualities for applications in the CPS domain. Brace strives to bound the computation overhead for CPS runtime verification while preserving a high level of monitoring accuracy in terms of the number of false positive and false negative reports. Brace is particularly suitable to systems in which scheduling is distributed across networked CPS components. We evaluate Brace to determine how effectively and efficiently it can detect injected errors in two existing real-life CPS applications with distributed scheduling. Our results demonstrate that Brace efficiently detects those errors and a few true bugs and is able to bound both the memory and computation overhead even in systems with large numbers of observed events.},\n  volume    = {12},\n  number    = {2},\n  pages     = {1667--1678},\n  year      = {2018},\n  url       = {https://doi.org/10.1109/JSYST.2016.2614599},\n  doi       = {10.1109/JSYST.2016.2614599},\n  timestamp = {Fri, 11 Sep 2020 15:02:08 +0200},\n  biburl    = {https://dblp.org/rec/journals/sj/Zheng0PCR18.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n
\n Our reliance on cyber-physical systems (CPSs) is increasingly widespread, but scalable methods for the analysis of such systems remain a significant challenge. Runtime verification of CPSs provides a reasonable middle ground between formal verification and simulation approaches, but it comes with its own challenges. A runtime verification system must run directly on the deployed application. In the CPS domain, it is therefore critical that a runtime verification system exhibits low overhead and good scalability so that the verification does not interfere with the analyzed CPS application. In this paper, we introduce Brace, a runtime verification system whose focus is on ensuring these performance qualities for applications in the CPS domain. Brace strives to bound the computation overhead for CPS runtime verification while preserving a high level of monitoring accuracy in terms of the number of false positive and false negative reports. Brace is particularly suitable to systems in which scheduling is distributed across networked CPS components. We evaluate Brace to determine how effectively and efficiently it can detect injected errors in two existing real-life CPS applications with distributed scheduling. Our results demonstrate that Brace efficiently detects those errors and a few true bugs and is able to bound both the memory and computation overhead even in systems with large numbers of observed events.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n WUPPAAL: Computation of Worst-Case Execution-Time for Binary Programs with UPPAAL.\n \n \n \n \n\n\n \n Cassez, F.; de Aledo, P. G.; and Jensen, P. G.\n\n\n \n\n\n\n In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460, of Lecture Notes in Computer Science, pages 560–577, 2017. Springer\n \n\n\n\n
\n\n\n\n \n \n \"WUPPAAL: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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mod-17,\n  author    = {Franck Cassez and\n               Pablo Gonz{\\'{a}}lez de Aledo and\n               Peter Gj{\\o}l Jensen},\n  title     = {{WUPPAAL:} Computation of Worst-Case Execution-Time for Binary Programs\n               with {UPPAAL}},\n  booktitle = {Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand\n               Larsen on the Occasion of His 60th Birthday},\n  pages     = {560--577},\n  year      = {2017},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10460},\n  publisher = {Springer},  \n  url       = {https://doi.org/10.1007/978-3-319-63121-9_28},\n  doi       = {10.1007/978-3-319-63121-9_28},\n  timestamp = {Tue, 22 Aug 2017 08:17:15 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/birthday/CassezAJ17},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n\n  urlpaper = {papers/kim-fest-17.pdf},\n  abstract = {We address the problem of computing the worst-case execu- tion-time (WCET) of binary programs using a real-time model-checker. \n  In our previous work, we introduced a fully automated and modular methodology to build a model (network of timed automata) that combined a binary \n  program and the hardware to run the program on. \n  Computing the WCET amounts to finding the longest path time-wise in this model, which can be done using a real-time model checker like Uppaal. \n  In this work, we generalise the previous approach and we define a generic framework to support arbitrary binary language and hardware.\nWe have implemented our new approach in an extended version of Uppaal, called Wuppaal. \nExperimental results using some standard benchmarks suite for WCET computation (from Malardalen University) \nshow that our technique is practical and promising.}\n}\n\n\n
\n
\n\n\n
\n We address the problem of computing the worst-case execu- tion-time (WCET) of binary programs using a real-time model-checker. In our previous work, we introduced a fully automated and modular methodology to build a model (network of timed automata) that combined a binary program and the hardware to run the program on. Computing the WCET amounts to finding the longest path time-wise in this model, which can be done using a real-time model checker like Uppaal. In this work, we generalise the previous approach and we define a generic framework to support arbitrary binary language and hardware. We have implemented our new approach in an extended version of Uppaal, called Wuppaal. Experimental results using some standard benchmarks suite for WCET computation (from Malardalen University) show that our technique is practical and promising.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Refinement of Trace Abstraction for Real-Time Programs.\n \n \n \n \n\n\n \n Cassez, F.; Jensen, P. G.; and Larsen, K. G.\n\n\n \n\n\n\n In Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings, volume 10506, pages 42–58, 2017. Springer\n \n\n\n\n
\n\n\n\n \n \n \"RefinementPaper\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 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rp-17,\n  author    = {Franck Cassez and\n               Peter Gj{\\o}l Jensen and\n               Kim Guldstrand Larsen},\n  title     = {Refinement of Trace Abstraction for Real-Time Programs},\n  booktitle = {Reachability Problems - 11th International Workshop, {RP} 2017, London,\n               UK, September 7-9, 2017, Proceedings},\n  volume    = {10506},\n  pages     = {42--58},\n  year      = {2017},\n  publisher = {Springer},\n  url       = {https://doi.org/10.1007/978-3-319-67089-8_4},\n  doi       = {10.1007/978-3-319-67089-8_4},\n  timestamp = {Wed, 30 Aug 2017 15:59:47 +0200},\n  isbn      = {978-3-319-67088-1},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/rp/CassezJL17},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  urlpaper = {papers/rp-17.pdf},\n  abstract = {Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. \n  They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. \n  We propose a semi-algorithm using refinement of trace abstractions to solve the reachability verification problem for real-time programs. \n  We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.}\n}\n\n\n
\n
\n\n\n
\n Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve the reachability verification problem for real-time programs. We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper).\n \n \n \n \n\n\n \n Cassez, F.; and Sloane, A.\n\n\n \n\n\n\n In SCALA'17, October 23–27, 2017, Vancouver, BC, Canada. Proceedings., 2017. acm\n forthcoming\n\n\n\n
\n\n\n\n \n \n \"ScalaSMT: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 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{scala-17,\nauthor    = {Franck Cassez\nand {Anthony M.} Sloane},\n  title     = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},\n  booktitle = {SCALA'17, October 23--27, 2017, Vancouver, BC, Canada. Proceedings.},\n  pages     = {},\n  year      = {2017},\n  xxxurl       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\n  xxxdoi       = {10.1007/978-3-662-46681-0_39},\n  publisher = "acm",\n  xvolume = 9035,\n  xxxseries    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {scala, SMT solvers},\n  category = {soft-verif},\n  show = {},\n  note={forthcoming},\n  urlpaper = {papers/scala-17.pdf},\n  abstract = {A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether \n  a logical formula is satisfiable. \n  The performance of SMT solvers has dramatically increased in the last decade and for instance, \n  many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. \n  We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. \n  ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. \n  Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, \n  thereby isolating users from the details of particular solvers.},\n    Type = {B - International Conferences},\n    show = {},\n}\n\n\n
\n
\n\n\n
\n A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether a logical formula is satisfiable. The performance of SMT solvers has dramatically increased in the last decade and for instance, many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, thereby isolating users from the details of particular solvers.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Real-Time Simulation Support for Runtime Verification of Cyber-Physical Systems.\n \n \n \n \n\n\n \n Zheng, X.; Julien, C.; Chen, H.; Podorozhny, R. M.; and Cassez, F.\n\n\n \n\n\n\n ACM Trans. Embed. Comput. Syst., 16(4): 106:1–106:24. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Real-TimePaper\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
@article{DBLP:journals/tecs/ZhengJCPC17,\n  author    = {Xi Zheng and\n               Christine Julien and\n               Hongxu Chen and\n               Rodion M. Podorozhny and\n               Franck Cassez},\n  title     = {Real-Time Simulation Support for Runtime Verification of Cyber-Physical\n               Systems},\n  journal   = {{ACM} Trans. Embed. Comput. Syst.},\n  volume    = {16},\n  number    = {4},\n  abstract={\n    In Cyber-Physical Systems (CPS), cyber and physical components must work seamlessly in tandem. Runtime verification of CPS is essential yet very difficult, due to deployment environments that are expensive, dangerous, or simply impossible to use for verification tasks. A key enabling factor of runtime verification of CPS is the ability to integrate real-time simulations of portions of the CPS into live running systems. We propose a verification approach that allows CPS application developers to opportunistically leverage real-time simulation to support runtime verification. Our approach, termed BraceBind, allows selecting, at runtime, between actual physical processes or simulations of them to support a running CPS application. To build BraceBind, we create a real-time simulation architecture to generate and manage multiple real-time simulation environments based on existing simulation models in a manner that ensures sufficient accuracy for verifying a CPS application. Specifically, BraceBind aims to both improve simulation speed and minimize latency, thereby making it feasible to integrate simulations of physical processes into the running CPS application. BraceBind then integrates this real-time simulation architecture with an existing runtime verification approach that has low computational overhead and high accuracy. This integration uses an aspect-oriented adapter architecture that connects the variables in the cyber portion of the CPS application with either sensors and actuators in the physical world or the automatically generated real-time simulation. Our experimental results show that, with a negligible performance penalty, our approach is both efficient and effective in detecting program errors that are otherwise only detectable in a physical deployment.\n  },\n  pages     = {106:1--106:24},\n  year      = {2017},\n  url       = {https://doi.org/10.1145/3063382},\n  doi       = {10.1145/3063382},\n  timestamp = {Fri, 09 Apr 2021 18:25:32 +0200},\n  biburl    = {https://dblp.org/rec/journals/tecs/ZhengJCPC17.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n
\n
\n\n\n
\n In Cyber-Physical Systems (CPS), cyber and physical components must work seamlessly in tandem. Runtime verification of CPS is essential yet very difficult, due to deployment environments that are expensive, dangerous, or simply impossible to use for verification tasks. A key enabling factor of runtime verification of CPS is the ability to integrate real-time simulations of portions of the CPS into live running systems. We propose a verification approach that allows CPS application developers to opportunistically leverage real-time simulation to support runtime verification. Our approach, termed BraceBind, allows selecting, at runtime, between actual physical processes or simulations of them to support a running CPS application. To build BraceBind, we create a real-time simulation architecture to generate and manage multiple real-time simulation environments based on existing simulation models in a manner that ensures sufficient accuracy for verifying a CPS application. Specifically, BraceBind aims to both improve simulation speed and minimize latency, thereby making it feasible to integrate simulations of physical processes into the running CPS application. BraceBind then integrates this real-time simulation architecture with an existing runtime verification approach that has low computational overhead and high accuracy. This integration uses an aspect-oriented adapter architecture that connects the variables in the cyber portion of the CPS application with either sensors and actuators in the physical world or the automatically generated real-time simulation. Our experimental results show that, with a negligible performance penalty, our approach is both efficient and effective in detecting program errors that are otherwise only detectable in a physical deployment. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Analysis of program code.\n \n \n \n \n\n\n \n Cassez, F.; and Müller, C.\n\n\n \n\n\n\n September 12 2017.\n US Patent 9,760,469\n\n\n\n
\n\n\n\n \n \n \"AnalysisPaper\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
@misc{cassez2017analysis,\n  title={Analysis of program code},\n  author={Cassez, F. and M{\\"u}ller, C.},\n  url={https://www.google.com/patents/US9760469},\n  year={2017},\n  mywebpage = {soft-verif},\n  abstract={\n  This disclosure relates to the analysis of a program based on source code where the source code comprises a call to a function associated with a function implementation. A processor determines, based on a summary that over-approximates the function, an assignment of an input variable and an output variable of the function call to reach a predefined state. The processor then determines, based on the implementation of the function whether the assignment of the input variable results in the assignment of the output variable. If it does not, the processor determines a narrowed summary for the function such that the narrowed summary over-approximates the function and excludes the assignment of the input variable and the output variable. Finally, the processor stores the narrowed summary on a datastore. Inlining of function code and unfolding of loops is avoided and parallel processing of multiple functions is possible.\n  },\n  keywords = {software verification},\n  category = {soft-verif},\n  month=sep # "~12",\n  note={US Patent 9,760,469}\n}\n\n\n\n
\n
\n\n\n
\n This disclosure relates to the analysis of a program based on source code where the source code comprises a call to a function associated with a function implementation. A processor determines, based on a summary that over-approximates the function, an assignment of an input variable and an output variable of the function call to reach a predefined state. The processor then determines, based on the implementation of the function whether the assignment of the input variable results in the assignment of the output variable. If it does not, the processor determines a narrowed summary for the function such that the narrowed summary over-approximates the function and excludes the assignment of the input variable and the output variable. Finally, the processor stores the narrowed summary on a datastore. Inlining of function code and unfolding of loops is avoided and parallel processing of multiple functions is possible. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution).\n \n \n \n \n\n\n \n Cassez, F.; Sloane, A.; Roberts, M.; Pigram, M.; Suvanpong, P.; and de Aledo Marugán, P. G.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. Proceedings, of lncs, pages 380–384, 2017. springv\n \n\n\n\n
\n\n\n\n \n \n \"Skink: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 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{tacas-17,\nauthor    = {Franck Cassez\nand {Anthony M.} Sloane\nand Matthew Roberts\nand Matthew Pigram\nand Pongsak Suvanpong\nand Pablo Gonz{\\'{a}}lez de Aledo Marug{\\'{a}}n},\n  title     = {Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution)},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n               - 23rd International Conference, {TACAS} 2017, Held as Part of the\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\n               2017, Uppsala, Sweden, April 22-29, 2017. Proceedings},\n  \n pages     = {380--384},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/978-3-662-54580-5_27},\n  doi       = {10.1007/978-3-662-54580-5_27},\n  publisher = springv,\n  xvolume = 10206,\n  series    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {refinement, software verification},\n  category = {soft-verif},\n  show = {},\n  xxnote={forthcoming},\n  urlpaper = {papers/sv-comp-2017.pdf},\n  abstract = {Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR)\nof a program source code.\nThe analysis consists of checking whether there is a feasible execution that can reach a\n designated error block in the LLVM-IR.\nThe result of a program analysis is ``correct'' if the error block is not reachable,\n``incorrect'' if the error block is reachable, or ``inconclusive'' if the status of the program could not be determined.\nIn this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.},\n    Type = {A - International Conferences},\n}\n\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2016\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n
\n
\n\n\n
\n Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR) of a program source code. The analysis consists of checking whether there is a feasible execution that can reach a designated error block in the LLVM-IR. The result of a program analysis is ``correct'' if the error block is not reachable, ``incorrect'' if the error block is reachable, or ``inconclusive'' if the status of the program could not be determined. In this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The Sbt-rats Parser Generator Plugin for Scala (Tool Paper).\n \n \n \n \n\n\n \n Sloane, A.; Cassez, F.; and Buckley, S.\n\n\n \n\n\n\n In Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, of SCALA 2016, pages 110–113, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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{scala-16,\n author = {Sloane, {Anthony M.} and Cassez, Franck and Buckley, Scott},\n title = {The {Sbt-rats} Parser Generator Plugin for Scala (Tool Paper)},\n booktitle = {Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala},\n series = {SCALA 2016},\n year = {2016},\n isbn = {978-1-4503-4648-1},\n location = {Amsterdam, Netherlands},\n pages = {110--113},\n numpages = {4},\n url = {http://doi.acm.org/10.1145/2998392.3001580},\n doi = {10.1145/2998392.3001580},\n urlpaper={papers/scala-2016.pdf},\n xxacmid = {3001580},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {Parsing expression grammars, Scala build tool},\n abstract={Tools for creating parsers are a key part of a mature language eco-system. Scala has traditionally relied on combinator libraries for defining parsers but being libraries they come with fundamental implementation limitations. An alternative is to use a Java-based parser generator such as ANTLR or Rats! but these tools are quite verbose and not ideal to use with Scala code. We describe our experiences with Scala-focused parser generation that is embodied in our sbtrats plugin for the Scala Build Tool. At its simplest, sbtrats provides a bridge to the Rats! parser generator for Java. On top of this bridge, we have a simple grammar definition notation that incorporates annotations for tree construction and pretty-printing. As well as generating a Rats! grammar, sbtrats can optionally generate case class definitions for the tree structure and a pretty-printer defined using our Kiama language processing library. We explain the sbtrats grammar notation and describe our positive experiences using it to define grammars for LLVM assembly notation and the SMTLIB input/output language for SMT solvers.},\n show = {},\n Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n Tools for creating parsers are a key part of a mature language eco-system. Scala has traditionally relied on combinator libraries for defining parsers but being libraries they come with fundamental implementation limitations. An alternative is to use a Java-based parser generator such as ANTLR or Rats! but these tools are quite verbose and not ideal to use with Scala code. We describe our experiences with Scala-focused parser generation that is embodied in our sbtrats plugin for the Scala Build Tool. At its simplest, sbtrats provides a bridge to the Rats! parser generator for Java. On top of this bridge, we have a simple grammar definition notation that incorporates annotations for tree construction and pretty-printing. As well as generating a Rats! grammar, sbtrats can optionally generate case class definitions for the tree structure and a pretty-printer defined using our Kiama language processing library. We explain the sbtrats grammar notation and describe our positive experiences using it to define grammars for LLVM assembly notation and the SMTLIB input/output language for SMT solvers.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient and Scalable Runtime Monitoring for Cyber–Physical System.\n \n \n \n \n\n\n \n Zheng, X.; Julien, C.; Podorozhny, R.; Cassez, F.; and Rakotoarivelo, T.\n\n\n \n\n\n\n IEEE Systems Journal, 99: 1–12. October 2016.\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n \n \"Efficient link\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
@article{ieee-16,\n  title={Efficient and Scalable Runtime Monitoring for Cyber--Physical System},\n  author={Zheng, Xi and Christine Julien and {Rodion M.} Podorozhny  and Franck Cassez and Thierry Rakotoarivelo},\n  journal={IEEE Systems Journal},\n  year={2016},\n  volume=99,\n  pages={1--12},\n  publisher={IEEE},\n  doi={10.1109/JSYST.2016.2614599},\n  ISSN={1932-8184},\n  urlpaper={papers/ieee-systems-2016.pdf},\n  url_link={http://ieeexplore.ieee.org/document/7605519/},\n  month=oct,\n  show = {},\n  keywords = {wcet, timed automata},\n\n  abstract={Our reliance on cyber–physical systems (CPSs) is increasingly widespread, but scalable methods for the analysis of such systems remain a significant challenge. Runtime verification of CPSs provides a reasonable middle ground between formal verification and simulation approaches, but it comes with its own challenges. A runtime verification system must run directly on the deployed application. In the CPS domain, it is therefore critical that a runtime verification system exhibits low overhead and good scalability so that the verification does not interfere with the analyzed CPS application. In this paper, we introduce Brace, a runtime verification system whose focus is on ensuring these performance qualities for applications in the CPS domain. Brace strives to bound the computation overhead for CPS runtime verification while preserving a high level of monitoring accuracy in terms of the number of false positive and false negative reports. Brace is particularly suitable to systems in which scheduling is distributed across networked CPS components. We evaluate Brace to determine how effectively and efficiently it can detect injected errors in two existing real-life CPS applications with distributed scheduling. Our results demonstrate that Brace efficiently detects those errors and a few true bugs and is able to bound both the memory and computation overhead even in systems with large numbers of observed events.},\n  Type = {A - Journal},\n\n}\n\n\n\n
\n
\n\n\n
\n Our reliance on cyber–physical systems (CPSs) is increasingly widespread, but scalable methods for the analysis of such systems remain a significant challenge. Runtime verification of CPSs provides a reasonable middle ground between formal verification and simulation approaches, but it comes with its own challenges. A runtime verification system must run directly on the deployed application. In the CPS domain, it is therefore critical that a runtime verification system exhibits low overhead and good scalability so that the verification does not interfere with the analyzed CPS application. In this paper, we introduce Brace, a runtime verification system whose focus is on ensuring these performance qualities for applications in the CPS domain. Brace strives to bound the computation overhead for CPS runtime verification while preserving a high level of monitoring accuracy in terms of the number of false positive and false negative reports. Brace is particularly suitable to systems in which scheduling is distributed across networked CPS components. We evaluate Brace to determine how effectively and efficiently it can detect injected errors in two existing real-life CPS applications with distributed scheduling. Our results demonstrate that Brace efficiently detects those errors and a few true bugs and is able to bound both the memory and computation overhead even in systems with large numbers of observed events.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The complexity of synchronous notions of information flow security.\n \n \n \n \n\n\n \n Cassez, F.; van der Meyden, R.; and Zhang, C.\n\n\n \n\n\n\n Theor. Comput. Sci., 631: 16–42. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n \n \"The link\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
@article{cassez-tcs-2016,\n  author    = {Franck Cassez and\n               Ron van der Meyden and\n               Chenyi Zhang},\n  title     = {The complexity of synchronous notions of information flow security},\n  journal   = {Theor. Comput. Sci.},\n  volume    = {631},\n  pages     = {16--42},\n  year      = {2016},\n  urlpaper = {papers/tcs-2016.pdf},\n  url_link       = {http://dx.doi.org/10.1016/j.tcs.2016.03.011},\n  doi       = {10.1016/j.tcs.2016.03.011},\n  timestamp = {Tue, 17 May 2016 17:26:44 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcs/CassezMZ16},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  show = {},\n  abstract={The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.},\n  Type = {A - Journal},\n  keywords = {security, non-interference},\n\n\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2015\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n BraceAssertion: Runtime Verification of Cyber-Physical Systems.\n \n \n \n \n\n\n \n Zheng, X.; Julien, C.; Podorozhny, R.; and Cassez, F.\n\n\n \n\n\n\n In 12th IEEE International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015, Dallas, TX, USA, October 19-22, 2015, pages 298–306, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"BraceAssertion:Paper\n  \n \n \n \"BraceAssertion: link\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{mass-Zheng-15,\n  author    = {Xi Zheng and\n               Christine Julien and\n               {Rodion M.} Podorozhny and\n               Franck Cassez},\n  title     = {BraceAssertion: Runtime Verification of Cyber-Physical Systems},\n  booktitle = {12th {IEEE} International Conference on Mobile Ad Hoc and Sensor Systems,\n               {MASS} 2015, Dallas, TX, USA, October 19-22, 2015},\n  pages     = {298--306},\n  year      = {2015},\n  urlpaper = {papers/mass-2015.pdf},\n  url_link       = {http://dx.doi.org/10.1109/MASS.2015.15},\n  doi       = {10.1109/MASS.2015.15},\n  timestamp = {Fri, 06 May 2016 13:36:43 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/mass/ZhengJPC15},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  show = {},\n  keywords = {wcet, timed automata},\n\n  abstract={Cyber-Physical Systems (CPS) have gained wide popularity, however, developing and debugging CPS remain significant challenges. Many bugs are detectable only at runtime under deployment conditions that may be unpredictable or at least unexpected at development time. The current state of the practice of debugging CPS is generally ad hoc, involving trial and error in a real deployment. For increased rigor, it is appealing to bring formal methods to CPS verification. However developers often eschew formal approaches due to complexity and lack of efficiency. This paper presents Brace Assertion, a specification framework based on natural language queries that are automatically converted to a determinitic class of timed automata used for runtime monitoring. To reduce runtime overhead and support properties that reference predicate logic, we use a second monitor automaton to create filtered traces on which to run the analysis using the specification monitor. We evaluate the Brace Assertion framework using a real CPS case study and show that the framework is able to minimize runtime overhead with an increasing number of monitors.},\n  Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n Cyber-Physical Systems (CPS) have gained wide popularity, however, developing and debugging CPS remain significant challenges. Many bugs are detectable only at runtime under deployment conditions that may be unpredictable or at least unexpected at development time. The current state of the practice of debugging CPS is generally ad hoc, involving trial and error in a real deployment. For increased rigor, it is appealing to bring formal methods to CPS verification. However developers often eschew formal approaches due to complexity and lack of efficiency. This paper presents Brace Assertion, a specification framework based on natural language queries that are automatically converted to a determinitic class of timed automata used for runtime monitoring. To reduce runtime overhead and support properties that reference predicate logic, we use a second monitor automaton to create filtered traces on which to run the analysis using the specification monitor. We evaluate the Brace Assertion framework using a real CPS case study and show that the framework is able to minimize runtime overhead with an increasing number of monitors.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timed Automata for Modelling Caches and Pipelines.\n \n \n \n \n\n\n \n Cassez, F.; and de Aledo Marugán, P. G.\n\n\n \n\n\n\n In van Glabbeek, R. J.; Groote, J. F.; and Höfner, P., editor(s), Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, November 23, 2015., volume 196, of EPTCS, pages 37–45, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"Timed link\n  \n \n \n \"TimedSlides\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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{cassez-mars-2015,\n  author    = {Franck Cassez and\n               Pablo Gonz{\\'{a}}lez de Aledo Marug{\\'{a}}n},\n  title     = {Timed Automata for Modelling Caches and Pipelines},\n  booktitle = {Proceedings Workshop on Models for Formal Analysis of Real Systems,\n               {MARS} 2015, Suva, Fiji, November 23, 2015.},\n  pages     = {37--45},\n  year      = {2015},\n   editor    = {Rob J. van Glabbeek and\n               Jan Friso Groote and\n               Peter H{\\"{o}}fner},\n                series    = {{EPTCS}},\n  volume    = {196},\n  year      = {2015},\n  url_link       = {http://dx.doi.org/10.4204/EPTCS.196.4},\n    urlslides = {papers/slides-mars-2015.pdf},\n  doi       = {10.4204/EPTCS.196.4},\n  category= {wcet},\n  mywebpage = {wcet},\n  show = {},\n  keywords = {wcet, timed automata},\n  abstract = {\n  In this paper, we focus on modelling the timing aspects of binary programs running on architectures featuring caches and pipelines. The objective is to obtain a timed automaton model to compute tight bounds for the worst-case execution time (WCET) of the programs using model-checking techniques.\n  },\n  Type = {B - International Conferences},\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we focus on modelling the timing aspects of binary programs running on architectures featuring caches and pipelines. The objective is to obtain a timed automaton model to compute tight bounds for the worst-case execution time (WCET) of the programs using model-checking techniques. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verification of Concurrent Programs Using Trace Abstraction Refinement.\n \n \n \n \n\n\n \n Cassez, F.; and Ziegler, F.\n\n\n \n\n\n\n In Davis, M.; Fehnker, A.; McIver, A.; and Voronkov, A., editor(s), Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450, of Lecture Notes in Computer Science, pages 233–248, 2015. Springer\n LPAR FMICS paper award\n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\n  \n \n \n \"VerificationSlides\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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{cassez-lpar-2015,\n  author    = {Franck Cassez and\n               Frowin Ziegler},\n                editor    = {Martin Davis and\n               Ansgar Fehnker and\n               Annabelle McIver and\n               Andrei Voronkov},\n  title     = {Verification of Concurrent Programs Using Trace Abstraction Refinement},\n  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th\n               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,\n               2015, Proceedings},\n  pages     = {233--248},\n  year      = {2015},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9450},\n  publisher = {Springer},\n  year      = {2015},\n  url       = {http://dx.doi.org/10.1007/978-3-662-48899-7_17},\n  mywebpage = {soft-verif},\n  category = {soft-verif},\n  isbn      = {978-3-662-48898-0},\n  doi       = {10.1007/978-3-662-48899-7_17},\n  show = {},\n  note = {LPAR FMICS  paper award},\n  urlpaper = {papers/lpar-2015.pdf},\n    urlslides = {papers/slides-lpar-2015.pdf},\n  abstract = {Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.},\n  Type = {B - International Conferences},\n}\n\n\n\n
\n
\n\n\n
\n Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution).\n \n \n \n \n\n\n \n Cassez, F.; Matsuoka, T.; Pierzchalski, E.; and Smyth, N.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035, of lncs, pages 439–442, 2015. springv\n \n\n\n\n
\n\n\n\n \n \n \"Perentie: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
@inproceedings{tacas-15,\nauthor    = {Franck Cassez and\n               Takashi Matsuoka and\n               Edward Pierzchalski and\n               Nathan Smyth},\n  title     = {Perentie: Modular Trace Refinement and Selective Value Tracking -\n               (Competition Contribution)},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n               - 21st International Conference, {TACAS} 2015, Held as Part of the\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\n               2015, London, UK, April 11-18, 2015. Proceedings},\n  pages     = {439--442},\n  year      = {2015},\n  url       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\n  doi       = {10.1007/978-3-662-46681-0_39},\n  publisher = springv,\n  volume = 9035,\n  series    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {refinement, software verification},\n  category = {soft-verif},\n  show = {},\n  urlpaper = {papers/sv-comp-2015.pdf},\n  abstract = {Perentie is a software analysis tool based on iterative refinement of trace abstraction:\n  if the refinement process terminates, the program is either declared correct or a counterexample is\n  provided and the program is incorrect.},\n    Type = {B - International Conferences},\n\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2014\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n Perentie is a software analysis tool based on iterative refinement of trace abstraction: if the refinement process terminates, the program is either declared correct or a counterexample is provided and the program is incorrect.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control and 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 International Journal of Control, 88(2): 217–236. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"ControlPaper\n  \n \n \n \"ControlLink\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
@article{ijc-14,\nauthor = {Benattar, Gilles and Franck Cassez and Lime, Didier\nand Roux, Olivier H.},\ntitle = {Control and Synthesis of Non-Interferent Timed\nSystems},\nType = {A - Journal},\njournal = {International Journal of Control}, \nvolume = {88}, \nnumber =\n{2},\npages = {217--236},\nyear = {2015},\ndoi = {10.1080/00207179.2014.944356},\nmywebpage = {timed},\nurlpaper = {papers/ijc-2014.pdf},\nee = {http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full},\nkeywords = {security, non-interference},\ncategory = {Non-interference},\nabstract = {We focus on the control and the\nsynthesis of secure timed systems which are modelled as timed automata. The\nsecurity property that the system must satisfy is a non-interference property.\nIntuitively, non-interference ensures the absence of any causal dependency from\na high-level domain to a lower level domain. Various notions of non-interference\nhave been defined in the literature, and in this paper, we focus on strong non-\ndeterministic non-interference (SNNI) and two (bi)simulation-based variants\nthereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties\nand their extensions have been mostly studied in the context of discrete event\nsystems, while it is now well-known that time is an important attack vector\nagainst secure systems. At the same time, there is an obvious interest in going\nbeyond simple verification to control problems: to be able to automatically make\nsystems secure. We consider non-interference properties in the challenging\nsetting of control of dense-time systems specified by timed automata and we\nstudy the two following problems: (1) check whether it is possible to find a\nsub-system so that it is non- interferent; if yes, (2) compute a (largest) sub-\nsystem which is non- interferent. We exhibit decidable sub-classes for these\nproblems, assess their theoretical complexities and provide effective algorithms\nbased on the classical framework of timed games.}\n}\n\n\n\n\n
\n
\n\n\n
\n We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. Various notions of non-interference have been defined in the literature, and in this paper, we focus on strong non- deterministic non-interference (SNNI) and two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems. At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure. We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non- interferent; if yes, (2) compute a (largest) sub- system which is non- interferent. We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings.\n \n \n \n \n\n\n \n Cassez, F.; and Raskin, J.,\n editors.\n \n\n\n \n\n\n\n Volume 8837, of lncs.springv. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\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
@proceedings{atva-14,\n  editor    = {Franck Cassez and\n               Jean-François Raskin},\n  title     = {Automated Technology for Verification and Analysis - 12th International\n               Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,\n               Proceedings},\n  series    = lncs,\n  volume    = {8837},\n  publisher = springv,\n  year      = {2014},\n  url       = {http://dx.doi.org/10.1007/978-3-319-11936-6},\n  doi       = {10.1007/978-3-319-11936-6},\n  show = {},\n  category = {Proceedings (Editor)},\n  isbn      = {978-3-319-11935-9},\n  Type = {D - Conference Proceedings},\n}\n\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Summary-Based Inter-Procedural Analysis via Modular Trace Refinement.\n \n \n \n \n\n\n \n Cassez, F.; Müller, C.; and Burnett, K.\n\n\n \n\n\n\n In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, pages 545–556, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"Summary-Based link\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{fsttcs-14,\n  author    = {Franck Cassez and\n               Christian Müller and\n               Karla Burnett},\n  title     = {Summary-Based Inter-Procedural Analysis via Modular Trace Refinement},\n  booktitle = {34th International Conference on Foundation of Software Technology\n               and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014,\n               New Delhi, India},\n  pages     = {545--556},\n  year      = {2014},\n  mywebpage = {soft-verif},\n  category = {Software verification},\n  keywords = {trace refinement, software verification, Hoare logic},\n  url_link       = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545},\n  doi       = {10.4230/LIPIcs.FSTTCS.2014.545},\n  abstract = {We propose a generalisation of trace refinement for the verification of inter-procedural programs.\n  Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand\n  and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a\n  modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the\n  main features of our approach and yields promising results.\n  },\n  Type = {B - International Conferences},\n}\n\n\n\n\n
\n
\n\n\n
\n We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Energy and mean-payoff timed games.\n \n \n \n \n\n\n \n Brenguier, R.; Cassez, F.; and Raskin, J.\n\n\n \n\n\n\n In 17th International Conference on Hybrid Systems: Computation and Control, HSCC'14, pages 283-292, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"EnergyPaper\n  \n \n \n \"Energy 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\n
\n
@inproceedings{hscc-14,\n  author    = {Romain Brenguier and\n               Franck Cassez and\n               Jean-François Raskin},\n  title     = {Energy and mean-payoff timed games},\n  booktitle = {17th International Conference on Hybrid Systems: Computation\n               and Control, HSCC'14},\n  year      = {2014},\n  pages     = {283-292},\n  urlpaper = {papers/hscc-2014.pdf},\n  url_link     = {http://doi.acm.org/10.1145/2562059.2562116},\n  mywebpage = {timed},\n  show = {},\n  keywords = {hybrid, timed automata, games},\n  abstract = {In this paper, we study energy and mean-payoff timed games.\n  The decision problems that consist in determining the existence of winning strategies in those games are undecidable,\n  and we thus provide semi-algorithms for solving these strategy synthesis problems.\n  We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete.\n  We also study in detail the relation between mean-payoff and energy timed games. Finally,\n  we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.},\n  Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we study energy and mean-payoff timed games. The decision problems that consist in determining the existence of winning strategies in those games are undecidable, and we thus provide semi-algorithms for solving these strategy synthesis problems. We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete. We also study in detail the relation between mean-payoff and energy timed games. Finally, we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Complexity of Synchronous Notions of Information Flow Security.\n \n \n \n \n\n\n \n Cassez, F.; van der Meyden, R.; and Zhang, C.\n\n\n \n\n\n\n CoRR, abs/1402.0601. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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\n
\n
@article{DBLP:journals/corr/CassezMZ14,\n  author    = {Franck Cassez and\n               Ron van der Meyden and\n               Chenyi Zhang},\n  title     = {The Complexity of Synchronous Notions of Information Flow Security},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1402.0601},\n  year      = {2014},\n  url       = {http://arxiv.org/abs/1402.0601},\n  timestamp = {Wed, 05 Mar 2014 14:43:44 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/CassezMZ14},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  keywords = {security, non-interference, complexity},\n  show = {},\n  category = {Non-interference},\n  abstract = {The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.\n  }\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2013\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (7)\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 67–105. Jard, C.; and Roux, O. H., editor(s). ISTE Ltd. – John Wiley & Sons, Ltd, February 2013.\n New edition, 2013\n\n\n\n
\n\n\n\n \n \n \"CommunicatingPaper\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
@inbook{cassez-control-iste-2013,\n   author = {Franck Cassez and Markey, Nicolas},\n   title = {Communicating Embedded Systems},\n   editor = {Jard, Claude and Roux, Olivier H.},\n   month = feb,\n   pages = {67--105},\n   publisher = {ISTE Ltd. -- John Wiley \\&amp; Sons, Ltd},\n   chapter = {Control of Timed Systems},\n  url = {http://onlinelibrary.wiley.com/book/10.1002/9781118558188},\n   year = {2013},\n   note = {New edition, 2013},\n   doi = {10.1002/9781118558188},\n   isbn = {9781848211438},\n   keywords = {control, timed automata},\n  mywbepage = {timed},\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. },\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 107–138. Jard, C.; and Roux, O. H., editor(s). ISTE Ltd. – John Wiley & Sons, Ltd, February 2013.\n New edition, 2013\n\n\n\n
\n\n\n\n \n \n \"CommunicatingPaper\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
@inbook{cassez-diag-iste-2013,\n   author = {Franck Cassez and Tripakis, Stavros},\n   title = {Communicating Embedded Systems},\n   editor = {Jard, Claude and Roux, Olivier H.},\n   month = feb,\n   pages = {107--138},\n   publisher = {ISTE Ltd. -- John Wiley \\&amp; Sons, Ltd},\n   chapter = {Fault Diagnosis of Timed Systems},\n   keywords = {diagnosis, timed automata},\n  mywbepage = {timed},\n  url = {http://onlinelibrary.wiley.com/book/10.1002/9781118558188},\n   year = {2013},\n      note = {New edition, 2013},\n    doi = {10.1002/9781118558188},\n   isbn = {9781848211438},\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.},\n                    Type = {C - Book Chapters},\n\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 Predictability of Event Occurrences in Timed Systems.\n \n \n \n \n\n\n \n Cassez, F.; and Grastien, A.\n\n\n \n\n\n\n In Formal Modeling and Analysis of Timed Systems - 11th International Conference, FORMATS 2013, Buenos Aires, Argentina, August 29-31, 2013. Proceedings, volume 8053, of Lecture Notes in Computer Science, pages 62–76, 2013. Springer\n \n\n\n\n
\n\n\n\n \n \n \"PredictabilityPaper\n  \n \n \n \"PredictabilitySlides\n  \n \n \n \"Predictability link\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 1 download\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{cassez-formats-2013,\n  author    = {Franck Cassez and\n               Alban Grastien},\n  title     = {Predictability of Event Occurrences in Timed Systems},\n  booktitle = {Formal Modeling and Analysis of Timed Systems - 11th International\n               Conference, {FORMATS} 2013, Buenos Aires, Argentina, August 29-31,\n               2013. Proceedings},\n  pages     = {62--76},\n  year      = {2013},\n  urlpaper = {papers/formats-2013.pdf},\n  urlslides = {papers/slides-formats-2013.pdf},\n   url_link       = {http://dx.doi.org/10.1007/978-3-642-40229-6_5},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {8053},\n  publisher = {Springer},\n  doi       = {10.1007/978-3-642-40229-6_5},\n  show = {},\n  keywords = {predictability, diagnosis, timed automata},\n  mywbepage = {timed},\n  category = {Fault diagnosis},\n  abstract = {\n    We address the problem of predicting events' occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event's occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events' occurrences in timed automata and show that the problem is PSPACE-complete.\n  },\n   Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n We address the problem of predicting events' occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event's occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events' occurrences in timed automata and show that the problem is PSPACE-complete. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n PtrTracker: Pragmatic pointer analysis.\n \n \n \n \n\n\n \n Biallas, S.; Olesen, M. C.; Cassez, F.; and Huuck, R.\n\n\n \n\n\n\n In 13th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2013, Eindhoven, Netherlands, September 22-23, 2013, pages 69–73, 2013. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"PtrTracker:Paper\n  \n \n \n \"PtrTracker: link\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{scam-2013,\n  author    = {Sebastian Biallas and\n               Mads Chr. Olesen and\n               Franck Cassez and\n               Ralf Huuck},\n  title     = {PtrTracker: Pragmatic pointer analysis},\n  booktitle = {13th {IEEE} International Working Conference on Source Code Analysis\n               and Manipulation, {SCAM} 2013, Eindhoven, Netherlands, September 22-23,\n               2013},\n  pages     = {69--73},\n  year      = {2013},\n  publisher = {{IEEE} Computer Society},\n  urlpaper = {papers/scam-2013.pdf},\n  url_link       = {http://dx.doi.org/10.1109/SCAM.2013.6648186},\n  doi       = {10.1109/SCAM.2013.6648186},\n  keywords = {Software verification, pointers, static analysis},\n  mywebpage = {soft-verif},\n  category = {Software verification},\n  abstract = {\n  Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed.\n  },\n    Type = {B - International Conferences},\n}\n\n\n\n
\n
\n\n\n
\n Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Predictability of Event Occurrences in Timed Systems.\n \n \n \n \n\n\n \n Cassez, F.; and Grastien, A.\n\n\n \n\n\n\n CoRR, abs/1306.0662. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"PredictabilityPaper\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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/CassezG13,\n  author    = {Franck Cassez and\n               Alban Grastien},\n  title     = {Predictability of Event Occurrences in Timed Systems},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1306.0662},\n  year      = {2013},\n  url       = {http://arxiv.org/abs/1306.0662},\n  timestamp = {Mon, 01 Jul 2013 20:31:24 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/CassezG13},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  category = {Fault diagnosis},\n  abstract = {\n  We address the problem of predicting events' occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event's occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events' occurrences in timed automata and show that the problem is PSPACE-complete.\n  },\n  mywebpage = {}\n}\n\n\n\n
\n
\n\n\n
\n We address the problem of predicting events' occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event's occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events' occurrences in timed automata and show that the problem is PSPACE-complete. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The expressive power of time Petri nets.\n \n \n \n \n\n\n \n Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n Theoretical Computer Science, 474: 1-20. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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
@article{tpn-13,\n  author    = {Béatrice Bérard and\n               Franck Cassez and\n               Serge Haddad and\n               Didier Lime and\n               Olivier H. Roux},\n  title     = {The expressive power of time {Petri} nets},\n  journal   =  {Theoretical Computer Science},\n  Type = {A - Journal},\n  volume    = {474},\n  year      = {2013},\n  pages     = {1-20},\n  doi        = {http://dx.doi.org/10.1016/j.tcs.2012.12.005},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  category= {Timed Petri nets},\n  mywebpage = {timed},\n  keywords = {time petri nets, timed automata},\n  urlpaper = {papers/tcs-2013.pdf},\n  abstract = {We investigate expressiveness questions for time Petri nets (TPNs)\n  and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs)\n  as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.\nWe give a syntactical translation from bounded GTPNs to timed automata (TA)\nthat generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l\ness expressive than TA w.r.t. weak timed bisimilarity.\nWe prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance.\nFinally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs "á la Merlin" w.r.t.\nweak timed bisimilarity. These results provide a unified comparison of the expressiveness of\nmany variants of timed models often used in practice. It leads to new important results for TPNs.\nAmong them are: 1-safe TPNs and bounded-TPNs are equally expressive; $\\epsilon$-transitions strictly\nincrease the expressive power of TPNs; self modifying nets as well as read,\ninhibitor and reset arcs do not add expressiveness to bounded TPNs.\n}\n}\n\n\n\n\n
\n
\n\n\n
\n We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l ess expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \"á la Merlin\" w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $ε$-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timing Analysis of Binary Programs with UPPAAL.\n \n \n \n \n\n\n \n Cassez, F.; and Béchennec, J.\n\n\n \n\n\n\n In 13th International Conference on Application of Concurrency to System Design, ACSD 2013, pages 41-50, July 2013. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"TimingPaper\n  \n \n \n \"TimingSlides\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 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{cassez-acsd-13,\n  author    = {Franck Cassez and\n               {Jean-Luc} Béchennec},\n  title     = {Timing Analysis of Binary Programs with {UPPAAL}},\n  booktitle = {13th International Conference on Application of Concurrency\n               to System Design, ACSD 2013},\n  year      = {2013},\n  month = jul,\n  pages     = {41-50},\n    PUBLISHER = {IEEE Computer Society},\n  urlpaper = {papers/acsd-2013.pdf},\n  urlslides = {papers/slides-acsd-wcet-2013.pdf},\n  doi       = {http://dx.doi.org/10.1109/ACSD.2013.7},\n  mywebpage = {wcet},\n  show = {},\n  keywords = {wcet, timed automata},\n  abstract = {\n  We address the problem of computing accurate Worst-Case Execution Time (WCET). We propose a fully automatic and modular methodology based on program slicing and real-time model-checking. We have implemented our methodology and applied it to standard benchmarks. To further validate the approach, we also compare our results to the real execution times of the programs measured on a real board.\n  },\n      Type = {B - International Conferences},\n\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2012\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n We address the problem of computing accurate Worst-Case Execution Time (WCET). We propose a fully automatic and modular methodology based on program slicing and real-time model-checking. We have implemented our methodology and applied it to standard benchmarks. To further validate the approach, we also compare our results to the real execution times of the programs measured on a real board. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012.\n \n \n \n \n\n\n \n Cassez, F.; Huuck, R.; Klein, G.; and Schlich, B.,\n editors.\n \n\n\n \n\n\n\n Volume 102, of EPTCS. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"ProceedingsPaper\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\n
\n
@proceedings{ssv-12,\n  editor    = {Franck Cassez and\n               Ralf Huuck and\n               Gerwin Klein and\n               Bastian Schlich},\n  title     = {Proceedings Seventh Conference on Systems Software Verification, {SSV}\n               2012, Sydney, Australia, 28-30 November 2012},\n  series    = {{EPTCS}},\n  volume    = {102},\n  year      = {2012},\n  url       = {http://dx.doi.org/10.4204/EPTCS.102},\n  doi       = {10.4204/EPTCS.102},\n  category= {Proceedings (Editor)},\n  mywebpage = {},\n  show = {},\n  keywords = {Proceedings},\n      Type = {D - Conference Proceedings},\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n What is a Timing Anomaly?.\n \n \n \n \n\n\n \n Cassez, F.; Hansen, R. R.; and Olesen, M. C.\n\n\n \n\n\n\n In 12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy, volume 23, of OASICS, pages 1-12, 2012. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik\n \n\n\n\n
\n\n\n\n \n \n \"WhatPaper\n  \n \n \n \"What 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
@inproceedings{wcet-12,\n  author    = {Franck Cassez and\n               René Rydhof Hansen and\n               Mads Chr. Olesen},\n  title     = {What is a Timing Anomaly?},\n  booktitle = {12th International Workshop on Worst-Case Execution Time\n               Analysis, WCET 2012, July 10, 2012, Pisa, Italy},\n  year      = {2012},\n  pages     = {1-12},\n  urlpaper = {papers/wcet-2012.pdf},\n  url_link        = {http://dx.doi.org/10.4230/OASIcs.WCET.2012.1},\n  abstract = {Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.},\n  category= {wcet},\n  mywebpage = {soft-verif,wcet},\n  keywords = {wcet},\n   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},\n  series    = {OASICS},\n  volume    = {23},\n        Type = {B - International Conferences},\n\n}\n\n\n\n\n
\n
\n\n\n
\n Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Controllers with Minimal Observation Power (Application to Timed Systems).\n \n \n \n \n\n\n \n Bulychev, P. E.; Cassez, F.; David, A.; Larsen, K. G.; Raskin, J.; and Reynier, P.\n\n\n \n\n\n\n In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, pages 223-237, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"ControllersPaper\n  \n \n \n \"Controllers 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 1 download\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{atva-12,\n  author    = {Peter E. Bulychev and\n               Franck Cassez and\n               Alexandre David and\n               Kim Guldstrand Larsen and\n               Jean-François Raskin and\n               Pierre-Alain Reynier},\n  title     = {Controllers with Minimal Observation Power (Application\n               to Timed Systems)},\n  booktitle = {Automated Technology for Verification and Analysis - 10th\n               International Symposium, ATVA 2012},\n  year      = {2012},\n  pages     = {223-237},\n  urlpaper = {papers/atva-2012.pdf},\n  url_link  = {http://dx.doi.org/10.1007/978-3-642-33386-6_19},\n  mywebpage = {timed},\n  keywords = {timed automata, timed games, control},\n  abstract = {\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\n  },\n        Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Controllers with Minimal Observation Power (Application to Timed Systems).\n \n \n \n \n\n\n \n Bulychev, P. E.; Cassez, F.; David, A.; Larsen, K. G.; Raskin, J.; and Reynier, P.\n\n\n \n\n\n\n CoRR, abs/1207.1276. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"ControllersPaper\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 1 download\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
@article{bulychev-2012,\n  author    = {Peter E. Bulychev and\n               Franck Cassez and\n               Alexandre David and\n               Kim G. Larsen and\n               Jean{-}Fran{\\c{c}}ois Raskin and\n               Pierre{-}Alain Reynier},\n  title     = {Controllers with Minimal Observation Power (Application to Timed Systems)},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1207.1276},\n  year      = {2012},\n  urlpaper       = {http://arxiv.org/abs/1207.1276},\n  timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-1276},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  abstract = {\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\n  },\n   mywebpage = {timed},\n  keywords = {timed automata, timed games, control},\n\n}\n\n\n\n
\n
\n\n\n
\n We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Complexity of Codiagnosability for Discrete Event and Timed Systems.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n IEEE Trans. Automat. Contr., 57(7): 1752-1764. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n \n \"The link\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 1 download\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
@article{tac-12,\n  author    = {Franck Cassez},\n  title     = {The Complexity of Codiagnosability for Discrete Event and\n               Timed Systems},\n  journal   = {IEEE Trans. Automat. Contr.},\n  volume    = {57},\n  number    = {7},\n  year      = {2012},\n  type = {A - Journal},\n  pages     = {1752-1764},\n  urlpaper = {papers/tac-2012.pdf},\n  url_link       = {http://dx.doi.org/10.1109/TAC.2012.2183169},\n  doi = {http://dx.doi.org/10.1109/TAC.2012.2183169},\n  mywebpage = {timed},\n  keywords = {timed automata, Fault diagnosis, Complexity},\n  abstract = {\n  In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete.\n  }\n}\n\n\n\n
\n
\n\n\n
\n In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of opaque systems with static and dynamic masks.\n \n \n \n \n\n\n \n Cassez, F.; Dubreil, J.; and Marchand, H.\n\n\n \n\n\n\n Formal Methods in System Design, 40(1): 88-115. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"SynthesisPaper\n  \n \n \n \"SynthesisLink\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\n
\n
@article{fmsd-12,\n  author    = {Franck Cassez and\n               Jérémy Dubreil and\n               Hervé Marchand},\n  title     = {Synthesis of opaque systems with static and dynamic masks},\n  journal   = {Formal Methods in System Design},\n  volume    = {40},\n  number    = {1},\n  year      = {2012},\n  pages     = {88-115},\n    type = {A - Journal},\n\n  urlpaper = {papers/fmsd-2012.pdf},\n  ee        = {http://dx.doi.org/10.1007/s10703-012-0141-9},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  mywebpage = {},\n  keywords = {security, opacity, diagnosis},\n  abstract = {\nOpacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.\n\n  },\n}\n\n\n\n
\n
\n\n\n
\n Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n High Performance Static Analysis for Industry.\n \n \n \n \n\n\n \n Bradley, M.; Cassez, F.; Fehnker, A.; Given-Wilson, T.; and Huuck, R.\n\n\n \n\n\n\n Electr. Notes Theor. Comput. Sci., 289: 3-14. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"HighPaper\n  \n \n \n \"HighLink\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
@article{tapas-12,\n  author    = {Mark Bradley and\n               Franck Cassez and\n               Ansgar Fehnker and\n               Thomas Given-Wilson and\n               Ralf Huuck},\n  title     = {High Performance Static Analysis for Industry},\n  journal   = {Electr. Notes Theor. Comput. Sci.},\n  volume    = {289},\n  year      = {2012},\n  pages     = {3-14},\n  urlpaper = {papers/tapas-2012.pdf},\n  ee        = {http://dx.doi.org/10.1016/j.entcs.2012.11.002},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  mywebpage = {soft-verif},\n  keywords = {software verification},\n  abstract = {\n  Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code.\n  },\n        Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control and 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 CoRR, abs/1207.4984. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"ControlPaper\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
@article{benattar-2012,\n  author    = {Gilles Benattar and\n               Franck Cassez and\n               Didier Lime and\n               Olivier H. Roux},\n  title     = {Control and Synthesis of Non-Interferent Timed Systems},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1207.4984},\n  year      = {2012},\n  url       = {http://arxiv.org/abs/1207.4984},\n  timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-4984},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  keywords = {sceurity, non-interference},\n  abstract = {\nIn this paper, we focus on the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower-level domain. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and two (bi)simulation based variants thereof (CSNNI and BSNNI). We consider timed non-interference properties for timed systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes (2) compute a (largest) sub-system which is non-interferent.\n  }\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2011\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n In this paper, we focus on the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower-level domain. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and two (bi)simulation based variants thereof (CSNNI and BSNNI). We consider timed non-interference properties for timed systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes (2) compute a (largest) sub-system which is non-interferent. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Timed Games for Computing WCET for Pipelined Processors with Caches.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011, pages 195–204, 2011. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"TimedPaper\n  \n \n \n \"TimedSlides\n  \n \n \n \"TimedLink\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{cassez-acsd-2011,\n  author    = {Franck Cassez},\n  title     = {Timed Games for Computing {WCET} for Pipelined Processors with Caches},\n  booktitle = {11th International Conference on Application of Concurrency to System\n               Design, {ACSD} 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011},\n  pages     = {195--204},\n  year      = {2011},\n  publisher = {{IEEE}},\n  url       = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.15},\n  doi       = {10.1109/ACSD.2011.15},\n  timestamp = {Wed, 15 Feb 2012 09:59:43 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/acsd/Cassez11},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n   urlpaper = {papers/acsd-2011.pdf},\n  urlslides = {papers/slides-acsd-2011.pdf},\n  ABSTRACT = {In this paper we introduce a framework for computing upper bounds yet\naccurate WCET for hardware platforms with caches and pipelines. The methodology\nwe propose consists of 3 steps: 1) given a program to analyse, compute an\nequivalent (WCET-wise) abstract program; 2) build a timed game by composing\nthis abstract program with a network of timed automata modeling the\narchitecture; and 3) compute the WCET as the optimal time to reach a winning\nstate in this game. We demonstrate the applicability of our framework on\nstandard benchmarks for an ARM9 processor with instruction and data caches, and\ncompute the WCET with UPPAAL-TiGA. We also show that this framework can easily\nbe extended to take into account dynamic changes in the speed of the processor\nduring program execution.\n},\nee       = {http://dx.doi.org/10.1109/ACSD.2011.15},\n  keywords = {wcet, timed automata},\n  category = {wcet},\n  show = {},\n  category= {wcet},\n  mywebpage = {wcet},\n        Type = {B - International Conferences},\n\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms with caches and pipelines. The methodology we propose consists of 3 steps: 1) given a program to analyse, compute an equivalent (WCET-wise) abstract program; 2) build a timed game by composing this abstract program with a network of timed automata modeling the architecture; and 3) compute the WCET as the optimal time to reach a winning state in this game. We demonstrate the applicability of our framework on standard benchmarks for an ARM9 processor with instruction and data caches, and compute the WCET with UPPAAL-TiGA. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Computation of WCET using Program Slicing and Real-Time Model-Checking.\n \n \n \n \n\n\n \n Béchennec, J.; and Cassez, F.\n\n\n \n\n\n\n CoRR, abs/1105.1633. 2011.\n \n\n\n\n
\n\n\n\n \n \n \"ComputationPaper\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
@article{bech-wcet-2011,\n  author    = {Jean{-}Luc B{\\'{e}}chennec and\n               Franck Cassez},\n  title     = {Computation of {WCET} using Program Slicing and Real-Time Model-Checking},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1105.1633},\n  year      = {2011},\n  urlpaper       = {http://arxiv.org/abs/1105.1633},\n  timestamp = {Mon, 05 Dec 2011 18:05:32 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1105-1633},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  ABSTRACT = { Computing accurate WCET on modern complex architectures is a challenging task. This problem has been devoted a lot of attention in the last decade but there are still some open issues. First, the control flow graph (CFG) of a binary program is needed to compute the WCET and this CFG is built using some internal knowledge of the compiler that generated the binary code; moreover once constructed the CFG has to be manually annotated with loop bounds. Second, the algorithms to compute the WCET (combining Abstract Interpretation and Integer Linear Programming) are tailored for specific architectures: changing the architecture (e.g. replacing an ARM7 by an ARM9) requires the design of a new ad hoc algorithm. Third, the tightness of the computed results (obtained using the available tools) are not compared to actual execution times measured on the real hardware. In this paper we address the above mentioned problems. We first describe a fully automatic method to compute a CFG based solely on the binary program to analyse. Second, we describe the model of the hardware as a product of timed automata, and this model is independent from the program description. The model of a program running on a hardware is obtained by synchronizing (the automaton of) the program with the (timed automata) model of the hardware. Computing the WCET is reduced to a reachability problem on the synchronised model and solved using the model-checker UPPAAL. Finally, we present a rigorous methodology that enables us to compare our computed results to actual execution times measured on a real platform, the ARM920T.},\n    category= {wcet},\n  keywords = {wcet, timed automata},\n  show = {},\n  mywebpage = {wcet}\n}\n\n\n\n
\n
\n\n\n
\n Computing accurate WCET on modern complex architectures is a challenging task. This problem has been devoted a lot of attention in the last decade but there are still some open issues. First, the control flow graph (CFG) of a binary program is needed to compute the WCET and this CFG is built using some internal knowledge of the compiler that generated the binary code; moreover once constructed the CFG has to be manually annotated with loop bounds. Second, the algorithms to compute the WCET (combining Abstract Interpretation and Integer Linear Programming) are tailored for specific architectures: changing the architecture (e.g. replacing an ARM7 by an ARM9) requires the design of a new ad hoc algorithm. Third, the tightness of the computed results (obtained using the available tools) are not compared to actual execution times measured on the real hardware. In this paper we address the above mentioned problems. We first describe a fully automatic method to compute a CFG based solely on the binary program to analyse. Second, we describe the model of the hardware as a product of timed automata, and this model is independent from the program description. The model of a program running on a hardware is obtained by synchronizing (the automaton of) the program with the (timed automata) model of the hardware. Computing the WCET is reduced to a reachability problem on the synchronised model and solved using the model-checker UPPAAL. Finally, we present a rigorous methodology that enables us to compare our computed results to actual execution times measured on a real platform, the ARM920T.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.\n \n \n \n \n\n\n \n Bouyer, P.; Cassez, F.; and Laroussinie, F.\n\n\n \n\n\n\n Journal of Logic, Language and Information, 20(2): 169–203. 2011.\n \n\n\n\n
\n\n\n\n \n \n \"TimedPaper\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\n
\n
@article{bouyer-jlli-2011,\n  author    = {Patricia Bouyer and\n               Franck Cassez and\n               Fran{\\c{c}}ois Laroussinie},\n  title     = {Timed Modal Logics for Real-Time Systems - Specification, Verification\n               and Control},\n  journal   = {Journal of Logic, Language and Information},\n  volume    = {20},\n  number    = {2},\n  pages     = {169--203},\n  year      = {2011},\n  Type = {A - Journal},\n  url       = {http://dx.doi.org/10.1007/s10849-010-9127-4},\n  doi       = {10.1007/s10849-010-9127-4},\n  timestamp = {Tue, 12 Apr 2011 09:14:59 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jolli/BouyerCL11},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  urlpaper = {papers/jlli-2011.pdf},\n  category= {games},\n  mywebpage = {timed},\n  show = {},\n  keywords = {logics, real-time, timed automata, timed games},\n  abstract = {\n  In this paper, a timed modal logic Lc is presented for the specification\nand verification of real-time systems. Several important results for Lc are discussed.\nFirst we address the model checking problem and we show that it is an EXPTIME-complete problem.\nSecondly we consider expressiveness and we explain how to\nexpress strong timed bisimilarity and how to build characteristic formulas for timed\nautomata. We also propose a compositional algorithm for Lc model checking. Finally\nwe consider several control problems for which Lc can be used to check controllability.\n  }\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2010\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n In this paper, a timed modal logic Lc is presented for the specification and verification of real-time systems. Several important results for Lc are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for Lc model checking. Finally we consider several control problems for which Lc can be used to check controllability. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The Complexity of Codiagnosability for Discrete Event and Timed Systems (Extended abstract).\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In Bouajjani, A.; and Chin, W., editor(s), Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, volume 6252, of Lecture Notes in Computer Science, pages 82–96, 2010. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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/atva/Cassez10,\n  author    = {Franck Cassez},\n  title     = {The Complexity of Codiagnosability for Discrete Event and Timed Systems (Extended abstract)},\n  booktitle = {Automated Technology for Verification and Analysis - 8th International\n               Symposium, {ATVA} 2010, Singapore, September 21-24, 2010. Proceedings},\n  pages     = {82--96},\n  year      = {2010},\n  editor    = {Ahmed Bouajjani and\n               Wei{-}Ngan Chin},\n  urlpaper = {papers/atva-10.pdf},\n  xxee = {http://arxiv.org/abs/1004.2550},\n  xxurl       = {http://dx.doi.org/10.1007/978-3-642-15643-4_8},\n  doi       = {10.1007/978-3-642-15643-4_8},\n series    = {Lecture Notes in Computer Science},\n  volume    = {6252},\n   mywebpage = {diagnosis},\n  show = {},\n  publisher = {Springer},\n  keywords = {diagnosis, complexity, timed automata},\n  abstract = {In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.},\n        Type = {B - International Conferences},\n\n  }\n\n\n\n
\n
\n\n\n
\n In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Dynamic Observers for Fault Diagnosis of Timed Systems.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In 49th IEEE Conference on Decision and Control and 28th Chinese Control Conference, Atlanta, December 2010. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"DynamicPaper\n  \n \n \n \"Dynamic 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
@INPROCEEDINGS{cassez-cdc-2010,\n  AUTHOR = {Franck Cassez},\n  TITLE = {{Dynamic Observers for Fault Diagnosis of Timed Systems}},\n  BOOKTITLE = {49th IEEE Conference on Decision and Control and 28th Chinese Control Conference},\n  YEAR = {2010},\n  ADDRESS = {Atlanta},\n  MONTH = DEC,\n  PUBLISHER = {IEEE Computer Society},\n  urlpaper = {papers/cdc-2010.pdf},\n  url_link = {http://arxiv.org/abs/1004.2764},\n  ABSTRACT = { In this paper we extend the work on dynamic observers for\nfault diagnosis  to timed automata. We\nstudy sensor minimization problems with static observers and\nthen address the problem of computing the most permissive\ndynamic observer for a system given by a timed automaton. },\n  mywebpage = {diagnosis},\n  show = {},\n  keywords = {diagnosis, timed automata},\n        Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n In this paper we extend the work on dynamic observers for fault diagnosis to timed automata. We study sensor minimization problems with static observers and then address the problem of computing the most permissive dynamic observer for a system given by a timed automaton. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Complexity of Synchronous Notions of Information Flow Security.\n \n \n \n \n\n\n \n Cassez, F.; van der Meyden, R.; and Zhang, C.\n\n\n \n\n\n\n In Ong, C. L., editor(s), Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014, of Lecture Notes in Computer Science, pages 282–296, 2010. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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{cassez-fossacs-2010,\n  author    = {Franck Cassez and\n               Ron van der Meyden and\n               Chenyi Zhang},\n               editor    = {C.{-}H. Luke Ong},\n  title     = {The Complexity of Synchronous Notions of Information Flow Security},\n  booktitle = {Foundations of Software Science and Computational Structures, 13th\n               International Conference, {FOSSACS} 2010, Held as Part of the Joint\n               European Conferences on Theory and Practice of Software, {ETAPS} 2010,\n               Paphos, Cyprus, March 20-28, 2010. Proceedings},\n  pages     = {282--296},\n  year      = {2010},\n  volume    = {6014},\n  urlpaper = {papers/fossacs-2010.pdf},\n  publisher = {Springer},\n  series    = {Lecture Notes in Computer Science},\n  doi       = {10.1007/978-3-642-12032-9_20},\n      keywords = {security, interference},\n      Type = {B - International Conferences},\n\n  abstract = {The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.}\n}\n\n\n\n
\n
\n\n\n
\n The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Complexity of Codiagnosability for Discrete Event and Timed Systems.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n CoRR, abs/1004.2550. 2010.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\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
@article{DBLP:journals/corr/abs-1004-2550,\n  author    = {Franck Cassez},\n  title     = {The Complexity of Codiagnosability for Discrete Event and Timed Systems},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1004.2550},\n  year      = {2010},\n  url       = {http://arxiv.org/abs/1004.2550},\n  timestamp = {Mon, 05 Dec 2011 18:05:32 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1004-2550},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n      keywords = {fault diagnosis, timed automata},\n\n  abstract = {In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.}\n}\n\n\n\n
\n
\n\n\n
\n In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.\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 CoRR, abs/1004.2764. 2010.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\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
@article{DBLP:journals/corr/abs-1004-2764,\n  author    = {Franck Cassez},\n  title     = {A Note on Fault Diagnosis Algorithms},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1004.2764},\n  year      = {2010},\n  url       = {http://arxiv.org/abs/1004.2764},\n  timestamp = {Mon, 05 Dec 2011 18:04:58 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1004-2764},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n      keywords = {fault diagnosis, timed automata},\n\n  abstract = {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\\"uchi 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 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 Fault Diagnosis with Dynamic Observers.\n \n \n \n \n\n\n \n Cassez, F.; and Tripakis, S.\n\n\n \n\n\n\n CoRR, abs/1004.2810. 2010.\n \n\n\n\n
\n\n\n\n \n \n \"FaultPaper\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
@article{DBLP:journals/corr/abs-1004-2810,\n  author    = {Franck Cassez and\n               Stavros Tripakis},\n  title     = {Fault Diagnosis with Dynamic Observers},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1004.2810},\n  year      = {2010},\n  url       = {http://arxiv.org/abs/1004.2810},\n  timestamp = {Mon, 05 Dec 2011 18:05:22 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1004-2810},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n    keywords = {fault diagnosis, timed automata},\n\n  abstract = {In this paper, we review some recent results about the use of dynamic observers for fault diagnosis of discrete event systems. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider dynamic observers: an observer can "switch" sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. We also solve the problem of dynamic observers' synthesis and prove that a most permissive observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer.}\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we review some recent results about the use of dynamic observers for fault diagnosis of discrete event systems. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider dynamic observers: an observer can \"switch\" sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. We also solve the problem of dynamic observers' synthesis and prove that a most permissive observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timed Games for Computing Worst-Case Execution-Times.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n CoRR, abs/1006.1951. 2010.\n \n\n\n\n
\n\n\n\n \n \n \"TimedPaper\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
@article{DBLP:journals/corr/abs-1006-1951,\n  author    = {Franck Cassez},\n  title     = {Timed Games for Computing Worst-Case Execution-Times},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1006.1951},\n  year      = {2010},\n  url       = {http://arxiv.org/abs/1006.1951},\n  timestamp = {Mon, 05 Dec 2011 18:04:54 +0100},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1006-1951},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n    keywords = {wcet, timed automata},\n\n  abstract= {In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms with caches and pipelines. The methodology we propose consists of 3 steps: 1) given a program to analyse, compute an equivalent (WCET-wise) abstract program; 2) build a timed game by composing this abstract program with a network of timed automata modeling the architecture; and 3) compute the WCET as the optimal time to reach a winning state in this game. We demonstrate the applicability of our framework on standard benchmarks for an ARM9 processor with instruction and data caches, and compute the WCET with UPPAAL-TiGA. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution.}\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2009\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms with caches and pipelines. The methodology we propose consists of 3 steps: 1) given a program to analyse, compute an equivalent (WCET-wise) abstract program; 2) build a timed game by composing this abstract program with a network of timed automata modeling the architecture; and 3) compute the WCET as the optimal time to reach a winning state in this game. We demonstrate the applicability of our framework on standard benchmarks for an ARM9 processor with instruction and data caches, and compute the WCET with UPPAAL-TiGA. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (8)\n \n \n
\n
\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 \"DynamicPaper\n  \n \n \n \"DynamicSlides\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 \"APaper\n  \n \n \n \"ASlides\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 \"SynthesisPaper\n  \n \n \n \"SynthesisSlides\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 \"AutomaticPaper\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 \"ThePaper\n  \n \n \n \"TheSlides\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 \"CommunicatingPaper\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 \\&amp; Sons, Ltd},\n   chapter = {Control of Timed Systems},\n  xxurl = {http://www.iste.co.uk/index.php?ACTION=Browse&amp;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 \"CommunicatingPaper\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 \\&amp; Sons, Ltd},\n   chapter = {Fault Diagnosis of Timed Systems},\n  xxurl = {http://www.iste.co.uk/index.php?ACTION=Browse&amp;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 \"HowPaper\n  \n \n \n \"How 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
\n
\n\n
\n
\n  \n 2008\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings.\n \n \n \n\n\n \n Cassez, F.; and Jard, C.,\n editors.\n \n\n\n \n\n\n\n Volume 5215, of Lecture Notes in Computer Science.springv. 2008.\n \n\n\n\n
\n\n\n\n \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
@proceedings{cassez-formats-2008,\n  editor    = {Franck Cassez and\n               Claude Jard},\n  title     = {Formal Modeling and Analysis of Timed Systems, 6th International Conference,\n               {FORMATS} 2008, Saint Malo, France, September 15-17, 2008. Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {5215},\n  publisher = springv,\n  year      = {2008},\n  isbn      = {978-3-540-85777-8},\n          Type = {D - Conference Proceedings},\n\n  timestamp = {Fri, 05 Sep 2008 08:05:45 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/formats/2008},\n  bibsource = {dblp computer science bibliography, http://dblp.org}\n}\n\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fault Diagnosis with Static and Dynamic Diagnosers.\n \n \n \n \n\n\n \n Cassez, F.; and Tripakis, S.\n\n\n \n\n\n\n Fundamenta Informaticae, 88(4): 497–540. November 2008.\n \n\n\n\n
\n\n\n\n \n \n \"FaultPaper\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
@article{cassez-fi-08,\n  AUTHOR = {Franck Cassez and Tripakis, Stavros},\n  TITLE = {Fault Diagnosis with Static and Dynamic Diagnosers},\n  JOURNAL = {Fundamenta Informaticae},\n  YEAR = {2008},\n    Type = {A - Journal},\n\n  VOLUME = {88},\n  NUMBER = {4},\n  PAGES = {497--540},\n  keywords = {fault diagnosis, automata},\n  MONTH = NOV,\n  ABSTRACT = {We study sensor minimization problems in the context of\n                  fault diagnosis. Fault diagnosis consists in\n                  synthesizing a diagnoser that observes a given plant\n                  and identifies faults in the plant as soon as\n                  possible after their occurrence. Existing literature\n                  on this problem has considered the case of fixed\n                  static observers, where the set of observable events\n                  is fixed and does not change during execution of the\n                  system. In this paper, we consider static observers\n                  where the set of observable events is not fixed, but\n                  needs to be optimized (e.g., minimized in size). We\n                  also consider dynamic observers, where the observer\n                  can ``switc'' sensors on or off, thus dynamically\n                  changing the set of events it wishes to observe. It\n                  is known that checking diagnosability (i.e., whether\n                  a given observer is capable of identifying faults)\n                  can be solved in polynomial time for static\n                  observers, and we show that the same is true for\n                  dynamic ones. On the other hand, minimizing the\n                  number of (static) observable events required to\n                  achieve diagnosability is NP-complete. We show that\n                  this is true also in the case of mask-based\n                  observation, where some events are observable but\n                  not distinguishable. For dynamic observers'\n                  synthesis, we prove that a most permissive\n                  finite-state observer can be computed in doubly\n                  exponential time, using a game-theoretic\n                  approach. We further investigate optimization\n                  problems for dynamic observers and define a notion of\n                  cost of an observer. We show how to compute an\n                  optimal observer using results on mean-payoff games\n                  by Zwick and Paterson.  },\n  urlpaper = {papers/diag-fi-08.pdf},\n}\n\n\n\n
\n
\n\n\n
\n We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider static observers where the set of observable events is not fixed, but needs to be optimized (e.g., minimized in size). We also consider dynamic observers, where the observer can ``switc'' sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. On the other hand, minimizing the number of (static) observable events required to achieve diagnosability is NP-complete. We show that this is true also in the case of mask-based observation, where some events are observable but not distinguishable. For dynamic observers' synthesis, we prove that a most permissive finite-state observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. We show how to compute an optimal observer using results on mean-payoff games by Zwick and Paterson. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?.\n \n \n \n \n\n\n \n Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n Theoretical Computer Science, 403(2–3): 202–220. 2008.\n \n\n\n\n
\n\n\n\n \n \n \"WhenPaper\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
@article{BCHLR08-tcs,\n  AUTHOR = {B{\\'e}rard, B{\\'e}atrice and Franck Cassez and Haddad, Serge and Lime, Didier and Roux, Olivier H.},\n  JOURNAL = {Theoretical Computer Science},\n  PUBLISHER = {Elsevier},\n  VOLUME = 403,\n  NUMBER = {2--3},\n  PAGES = {202--220},\n    Type = {A - Journal},\n\n  TITLE = {When are Timed Automata Weakly Timed Bisimilar to Time {P}etri Nets?},\n  YEAR = {2008},\n  urlpaper = {papers/tcs-2008.pdf},\n  abstract = {In this paper, we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem  are PSPACE-complete. Furthermore we show that for a TA in this class with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.}\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper, we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem are PSPACE-complete. Furthermore we show that for a TA in this class with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Petri Nets – Theory and Applications.\n \n \n \n \n\n\n \n Cassez, F.; and Roux, O. H.\n\n\n \n\n\n\n of I-Tech Education Online. Petri Nets – Theory and Applications, pages 225–252. Kordic, V., editor(s). ARS-VIENNA, 2008.\n Free download from ˘rlhttp://intechweb.org/books.php.\n\n\n\n
\n\n\n\n \n \n \"PetriPaper\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{ars-petri-nets,\n  AUTHOR = {Cassez, Franck and Roux, Olivier H.},\n  EDITOR = {Kordic, Vedran},\n  TITLE = {Petri Nets -- Theory and Applications},\n  CHAPTER = {From Time Petri Nets to Timed Automata},\n  PUBLISHER = ARS-VIENNA,\n  YEAR = {2008},\n  SERIES = {{I}-Tech {E}ducation {O}nline},\n URL= {http://intechweb.org/books.php},\n  PAGES = {225--252},\n  PDF = {papers/tpn-book-08.pdf},\n  ISBN = {ISBN 978-3-902613-12-7},\nNOTE={Free download from \\url{http://intechweb.org/books.php}.},\n  ABSTRACT = {In this chapter we introduce a formalism, \\emph{Time\n                  Petri Nets (TPNs)}, to model real-time systems. We\n                  compare it with another well-known formalism,\n                  \\emph{Timed Automata (TA)}, used for specifying\n                  timed systems.  We precisely define the semantics of\n                  TPNs and TA and compare them according to two\n                  criteria: the \\emph{languages} (or set of\n                  behaviours) then can generate, and the \\emph{trees}\n                  (or branching behaviours) they can generate.  We\n                  show that every TPN can be translated into an\n                  equivalent TA.  Then, we introduce a real-time logic\n                  to specify properties of real-time systems. We show\n                  how to check that a given TPN satisfies a property\n                  written in this logic. For this we use our\n                  translation\\footnote{This translation preserves the\n                  properties of this logic.} from TPNs to TA and check\n                  the property on the equivalent TA. Finally we\n                  briefly report on experiments for checking real-time\n                  properties of TPNs using this framework. },\n    Type = {C - Book Chapters},\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2007\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n\n
\n
\n\n\n
\n In this chapter we introduce a formalism, \\emphTime Petri Nets (TPNs), to model real-time systems. We compare it with another well-known formalism, \\emphTimed Automata (TA), used for specifying timed systems. We precisely define the semantics of TPNs and TA and compare them according to two criteria: the \\emphlanguages (or set of behaviours) then can generate, and the \\emphtrees (or branching behaviours) they can generate. We show that every TPN can be translated into an equivalent TA. Then, we introduce a real-time logic to specify properties of real-time systems. We show how to check that a given TPN satisfies a property written in this logic. For this we use our translation\\footnoteThis translation preserves the properties of this logic. from TPNs to TA and check the property on the equivalent TA. Finally we briefly report on experiments for checking real-time properties of TPNs using this framework. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Semantics of Biological Regulatory Networks.\n \n \n \n \n\n\n \n Bernot, G.; Cassez, F.; Comet, J.; Delaplace, F.; Müller, C.; Roux, O.; and Roux, O.\n\n\n \n\n\n\n Electr. Notes Theor. Comput. Sci. (Proceedings of FORMATS 2003), 180(3): 3–14. 2007.\n \n\n\n\n
\n\n\n\n \n \n \"SemanticsPaper\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 1 download\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
@article{DBLP:journals/entcs/BernotCCDMR07,\n  author    = {Gilles Bernot and\n               Franck Cassez and\n               Jean{-}Paul Comet and\n               Franck Delaplace and\n               C{\\'{e}}line M{\\"{u}}ller and\n               {Olivier F.} Roux and {Olivier H.} Roux},\n  title     = {Semantics of Biological Regulatory Networks},\n  journal   = {Electr. Notes Theor. Comput. Sci. (Proceedings of FORMATS 2003)},\n  volume    = {180},\n  number    = {3},\n  pages     = {3--14},\n  year      = {2007},\n  url       = {http://dx.doi.org/10.1016/j.entcs.2004.01.038},\n  doi       = {10.1016/j.entcs.2004.01.038},\n  keywords = {bioinformatics, regulatory networks, hybrid systems},\n  abstract ={The aim of the paper is to revisit the model of Biological Regulatory Networks (BRN) which was proposed by René Thomas to model the interactions between a set of genes. We give a formal semantics for BRN in terms of transition systems which formalizes the evolution rules given by René Thomas. Then we show how to use this model to find interesting properties of a BRN like the set of stable states, cycles etc using tools for analyzing transition systems.},\n          Type = {B - International Conferences},\n\n}\n\n\n\n
\n
\n\n\n
\n The aim of the paper is to revisit the model of Biological Regulatory Networks (BRN) which was proposed by René Thomas to model the interactions between a set of genes. We give a formal semantics for BRN in terms of transition systems which formalizes the evolution rules given by René Thomas. Then we show how to use this model to find interesting properties of a BRN like the set of stable states, cycles etc using tools for analyzing transition systems.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis.\n \n \n \n \n\n\n \n Cassez, F.; Tripakis, S.; and Altisen, K.\n\n\n \n\n\n\n In Basten, T.; Juhás, G.; and Shukla, S. K., editor(s), Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), 10-13 July 2007, Bratislava, Slovak Republic, pages 90–99, 2007. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"SensorPaper\n  \n \n \n \"SensorSlides\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{CassezTA07,\n  author    = {Franck Cassez and\n               Stavros Tripakis and\n               Karine Altisen},\n  title     = {Sensor Minimization Problems with Static or Dynamic Observers for\n               Fault Diagnosis},\n  booktitle = {Seventh International Conference on Application of Concurrency to\n               System Design {(ACSD} 2007), 10-13 July 2007, Bratislava, Slovak Republic},\n  pages     = {90--99},\n  year      = {2007},\n  editor    = {Twan Basten and\n               Gabriel Juh{\\'{a}}s and\n               Sandeep K. Shukla},\n  crossref  = {DBLP:conf/acsd/2007},\n  url       = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2007.65},\n  doi       = {10.1109/ACSD.2007.65},\n  publisher = {{IEEE} Computer Society},\n  year      = {2007},\n  keyworfs = {fault diagnosis, automata},\n  urlpaper = {papers/acsd07.pdf},\n          Type = {B - International Conferences},\n\n  urlslides = {papers/slides-acsd-07.pdf},\n  abstract = {We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe.}\n}\n\n\n\n
\n
\n\n\n
\n We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timed Control with Observation Based and Stuttering Invariant Strategies.\n \n \n \n \n\n\n \n Cassez, F.; David, A.; Larsen, K. G.; Lime, D.; and Raskin, J.\n\n\n \n\n\n\n In Namjoshi, K. S.; Yoneda, T.; Higashino, T.; and Okamura, Y., editor(s), Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, volume 4762, of Lecture Notes in Computer Science, pages 192–206, 2007. Springer\n \n\n\n\n
\n\n\n\n \n \n \"TimedPaper\n  \n \n \n \"Timed link\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{CassezDLLR07,\n  author    = {Franck Cassez and\n               Alexandre David and\n               Kim Guldstrand Larsen and\n               Didier Lime and\n               Jean{-}Fran{\\c{c}}ois Raskin},\n  title     = {Timed Control with Observation Based and Stuttering Invariant Strategies},\n  booktitle = {Automated Technology for Verification and Analysis, 5th International\n               Symposium, {ATVA} 2007, Tokyo, Japan, October 22-25, 2007, Proceedings},\n  pages     = {192--206},\n  year      = {2007},\n          Type = {B - International Conferences},\n\n  editor    = {Kedar S. Namjoshi and\n               Tomohiro Yoneda and\n               Teruo Higashino and\n               Yoshio Okamura},\n   series    = {Lecture Notes in Computer Science},\n  volume    = {4762},\n  publisher = {Springer},\n  urlpaper  = {papers/atva-07.pdf},\n  url_link       = {http://dx.doi.org/10.1007/978-3-540-75596-8_15},\n  doi       = {10.1007/978-3-540-75596-8_15},\n  abstract = {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 finite collection of observations and must be stuttering invariant in the sense that repeated identical observations will not change the strategy. We provide a constructive transformation to equivalent finite games with perfect infor- mation, giving decidability as well as allowing for an efficient on-the-fly forward algorithm. We report on application of an initial experimental implementation.},\n  keywords = {control, timed automata, partial observation}\n}\n\n\n\n\n
\n
\n\n\n
\n 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 finite collection of observations and must be stuttering invariant in the sense that repeated identical observations will not change the strategy. We provide a constructive transformation to equivalent finite games with perfect infor- mation, giving decidability as well as allowing for an efficient on-the-fly forward algorithm. We report on application of an initial experimental implementation.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient On-the-Fly Algorithms for Partially Observable Timed Games.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n In Raskin, J.; and Thiagarajan, P. S., editor(s), Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, volume 4763, of Lecture Notes in Computer Science, pages 5–24, 2007. Springer\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n \n \"EfficientSlides\n  \n \n \n \"Efficient link\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{cassez-formats-07,\n  author    = {Franck Cassez},\n  title     = {Efficient On-the-Fly Algorithms for Partially Observable Timed Games},\n  booktitle = {Formal Modeling and Analysis of Timed Systems, 5th International Conference,\n               {FORMATS} 2007, Salzburg, Austria, October 3-5, 2007, Proceedings},\n  pages     = {5--24},\n  year      = {2007},\n  editor    = {Jean{-}Fran{\\c{c}}ois Raskin and\n               P. S. Thiagarajan},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {4763},\n          Type = {B - International Conferences},\n\n  publisher = {Springer},\n  urlpaper = {papers/formats-07.pdf},\n  urlslides = {papers/formats-07-slides.pdf},\n  url_link       = {http://dx.doi.org/10.1007/978-3-540-75454-1_3},\n  doi       = {10.1007/978-3-540-75454-1_3},\n  abstract = { In this paper, we review some recent results on the efficient synthesis of controllers for timed systems. We first recall the basics of controller synthesis for timed games and then present an efficient on-the-fly algorithm for reachability games and its extension to partially observable timed games.},\n  keywords = {control, timed automata}\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we review some recent results on the efficient synthesis of controllers for timed systems. We first recall the basics of controller synthesis for timed games and then present an efficient on-the-fly algorithm for reachability games and its extension to partially observable timed games.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems.\n \n \n \n \n\n\n \n Cassez, F.; Tripakis, S.; and Altisen, K.\n\n\n \n\n\n\n In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007, June 5-8, 2007, Shanghai, China, pages 316–325, 2007. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"SynthesisPaper\n  \n \n \n \"SynthesisSlides\n  \n \n \n \"Synthesis link\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/tase/CassezTA07,\n  author    = {Franck Cassez and\n               Stavros Tripakis and\n               Karine Altisen},\n  title     = {Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of\n               Discrete-Event Systems},\n  booktitle = {First Joint {IEEE/IFIP} Symposium on Theoretical Aspects of Software\n               Engineering, {TASE} 2007, June 5-8, 2007, Shanghai, China},\n  publisher = {{IEEE} Computer Society},\n   pages     = {316--325},\n  year      = {2007},\n          Type = {B - International Conferences},\n\n  urlpaper = {papers/tase-07.pdf},\n  urlslides = {papers/slides-tase-07.pdf},\n  url_link       = {http://dx.doi.org/10.1109/TASE.2007.51},\n  isbn      = {0-7695-2856-2},\n  doi       = {10.1109/TASE.2007.51},\n  abstract = {Fault diagnosis consists in synthesizing a diagnoser that observes a given plant through a set of observable events, and identifies faults which are not observable as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe. We define a notion of cost for such dynamic observers and show that (i) the cost of a given dynamic observer can be computed and (ii) an optimal dynamic observer can be synthesized.},\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2006\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n\n
\n
\n\n\n
\n Fault diagnosis consists in synthesizing a diagnoser that observes a given plant through a set of observable events, and identifies faults which are not observable as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe. We define a notion of cost for such dynamic observers and show that (i) the cost of a given dynamic observer can be computed and (ii) an optimal dynamic observer can be synthesized.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Structural Translation from Time Petri Nets to Timed Automata.\n \n \n \n \n\n\n \n Cassez, F.; and Roux, O. H.\n\n\n \n\n\n\n Journal of Software and Systems, 79(10): 1456–1468. October 2006.\n \n\n\n\n
\n\n\n\n \n \n \"StructuralPaper\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\n
\n
@article{cassez-jss-06,\n  ABSTRACT = {In this paper, we consider Time Petri Nets (TPN)\n                  where time is associated with transitions. We give a\n                  formal semantics for TPNs in terms of Timed\n                  Transition Systems. Then, we propose a translation\n                  from TPNs to Timed Automata (TA) that preserves the\n                  behavioral semantics (timed bisimilarity) of the\n                  TPNs. For the theory of TPNs this result is\n                  two-fold: i) reachability problems and more\n                  generally TCTL model-checking are decidable for\n                  bounded TPNs; ii) allowing strict time constraints\n                  on transitions for TPNs preserves the results\n                  described in i). The practical appli- cations of the\n                  translation are: i) one can specify a system using\n                  both TPNs and Timed Automata and a precise semantics\n                  is given to the composition; ii) one can use\n                  existing tools for analyzing timed automata (like\n                  Kronos, Uppaal or Cmc) to analyze TPNs. In this\n                  paper we describe the new feature of the tool Romeo\n                  that implements our translation of TPNs in the\n                  Uppaal input format. We also report on experiments\n                  carried out on various examples and compare the\n                  result of our method to state-of-the-art tool for\n                  analyzing TPNs.  },\n  AUTHOR = {Franck Cassez and Roux, Olivier Henri},\n  JOURNAL = {Journal of Software and Systems},\n  Type = {A - Journal},\n  PAGES = {1456--1468},\n  urlpaper = {papers/jss-06.pdf},\n  TITLE = {Structural Translation from Time Petri Nets to Timed Automata},\n  VOLUME = {79},\n  NUMBER = {10},\n  MONTH = OCT,\n  PUBLISHER = {Elsevier},\n  YEAR = {2006},\n  keywords = {Time Petri nets, timed automata, expressiveness}\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioral semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical appli- cations of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analyzing timed automata (like Kronos, Uppaal or Cmc) to analyze TPNs. In this paper we describe the new feature of the tool Romeo that implements our translation of TPNs in the Uppaal input format. We also report on experiments carried out on various examples and compare the result of our method to state-of-the-art tool for analyzing TPNs. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Monitoring and fault-diagnosis with digital clocks.\n \n \n \n \n\n\n \n Altisen, K.; Cassez, F.; and Tripakis, S.\n\n\n \n\n\n\n In Sixth International Conference on Application of Concurrency to System Design (ACSD 2006), 28-30 June 2006, Turku, Finland, pages 101–110, 2006. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"MonitoringPaper\n  \n \n \n \"MonitoringSlides\n  \n \n \n \"Monitoring link\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/acsd/AltisenCT06,\n  author    = {Karine Altisen and\n               Franck Cassez and\n               Stavros Tripakis},\n  title     = {Monitoring and fault-diagnosis with digital clocks},\n  booktitle = {Sixth International Conference on Application of Concurrency to System\n               Design {(ACSD} 2006), 28-30 June 2006, Turku, Finland},\n  pages     = {101--110},\n  year      = {2006},\n  publisher = {{IEEE} Computer Society},\n  urlpaper = {papers/acsd06.pdf},\n  urlslides = {papers/slides-acsd-06.pdf},\n  url_link       = {http://dx.doi.org/10.1109/ACSD.2006.10},\n  doi       = {10.1109/ACSD.2006.10},\n          Type = {B - International Conferences},\n\n  abstract = {\nWe study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification mod- eled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diag- nosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability.},\n  keywords = {fault diagnosis, timed automata, monitoring}\n}\n\n\n\n
\n
\n\n\n
\n We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification mod- eled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diag- nosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Symbolic Unfoldings for Networks of Timed Automata.\n \n \n \n \n\n\n \n Cassez, F.; Chatain, T.; and Jard, C.\n\n\n \n\n\n\n In Graf, S.; and Zhang, W., editor(s), Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006., volume 4218, of Lecture Notes in Computer Science, pages 307–321, 2006. Springer\n \n\n\n\n
\n\n\n\n \n \n \"SymbolicPaper\n  \n \n \n \"SymbolicSlides\n  \n \n \n \"Symbolic link\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/atva/CassezCJ06,\n  author    = {Franck Cassez and\n               Thomas Chatain and\n               Claude Jard},\n  editor    = {Susanne Graf and\n               Wenhui Zhang},\n  title     = {Symbolic Unfoldings for Networks of Timed Automata},\n  booktitle = {Automated Technology for Verification and Analysis, 4th International\n               Symposium, {ATVA} 2006, Beijing, China, October 23-26, 2006.},\n  pages     = {307--321},\n  year      = {2006},\n          Type = {B - International Conferences},\n\n  series    = {Lecture Notes in Computer Science},\n  volume    = {4218},\n  publisher = {Springer},\n  urlpaper = {papers/unfolding-rr-06.pdf},\n  urlslides = {papers/slides-atva-06.pdf},\n  url_link       = {http://dx.doi.org/10.1007/11901914_24},\n  doi       = {10.1007/11901914_24},\n  abstract = {In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.},\n  keywords = {unfoldings, timed automata},\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2005\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n\n
\n
\n\n\n
\n In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Structural Translation from Time Petri Nets to Timed Automata.\n \n \n \n \n\n\n \n Cassez, F.; and Roux, O. H.\n\n\n \n\n\n\n Electr. Notes Theor. Comput. Sci. (Proceedings of AVOCS 2004), 128(6): 145–160. 2005.\n \n\n\n\n
\n\n\n\n \n \n \"StructuralPaper\n  \n \n \n \"StructuralSlides\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
@article{DBLP:journals/entcs/CassezR05,\n  author    = {Franck Cassez and\n               Olivier H. Roux},\n  title     = {Structural Translation from Time Petri Nets to Timed Automata},\n  journal   = {Electr. Notes Theor. Comput. Sci. (Proceedings of AVOCS 2004)},\n  volume    = {128},\n          Type = {B - International Conferences},\n  number    = {6},\n  pages     = {145--160},\n  year      = {2005},\n  url       = {http://dx.doi.org/10.1016/j.entcs.2005.04.009},\n  doi       = {10.1016/j.entcs.2005.04.009},\n  urlslides = {papers/slides-avocs-04.pdf},\n\n  abstract = {In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.},\n  keywords = {Petri nets, timed, automata},\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Comparison of Different Semantics for Time Petri Nets.\n \n \n \n \n\n\n \n Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n In Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707, of Lecture Notes in Computer Science, pages 293–307, 2005. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ComparisonPaper\n  \n \n \n \"Comparison link\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/atva/BerardCHLR05,\n  author    = {B{\\'{e}}atrice B{\\'{e}}rard and\n               Franck Cassez and\n               Serge Haddad and\n               Didier Lime and\n               Olivier H. Roux},\n  title     = {Comparison of Different Semantics for Time Petri Nets},\n  booktitle = {Automated Technology for Verification and Analysis, Third International Symposium, {ATVA} 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {3707},\n  publisher = {Springer},\n  pages     = {293--307},\n          Type = {B - International Conferences},\n\n  year      = {2005},\n  urlpaper = {papers/petri-nets-atva05.pdf},\n  url_link       = {http://dx.doi.org/10.1007/11562948_23},\n  doi       = {10.1007/11562948_23},\n  abstract = {In this paper we study the model of Time Petri Nets (TPNs) where a time interval is associated with the firing of a transition, but we extend it by considering general intervals rather than closed ones. A key feature of timed models is the memory policy, i.e. which timing informations are kept when a transition is fired. The original model selects an intermediate semantics where the transitions disabled after consuming the tokens, as well as the firing transition, are reinitialised. However this semantics is not appropriate for some applications. So we consider here two alternative semantics: the atomic and the persistent atomic ones. First we present relevant patterns of discrete event systems which show the interest of these semantics. Then we compare the expressiveness of the three semantics w.r.t. the weak time bisimilarity establishing inclusion results in the general case. Furthermore we show that some inclusions are strict with unrestricted intervals even when nets are bounded. Then we focus on bounded TPNs with upper-closed intervals and we prove that the semantics are equivalent. Finally taking into account both the practical and the theoretical issues, we conclude that persistent atomic semantics should be preferred.},\n  keywords = {Petri nets, semantics, expressiveness}\n}\n\n\n\n
\n
\n\n\n
\n In this paper we study the model of Time Petri Nets (TPNs) where a time interval is associated with the firing of a transition, but we extend it by considering general intervals rather than closed ones. A key feature of timed models is the memory policy, i.e. which timing informations are kept when a transition is fired. The original model selects an intermediate semantics where the transitions disabled after consuming the tokens, as well as the firing transition, are reinitialised. However this semantics is not appropriate for some applications. So we consider here two alternative semantics: the atomic and the persistent atomic ones. First we present relevant patterns of discrete event systems which show the interest of these semantics. Then we compare the expressiveness of the three semantics w.r.t. the weak time bisimilarity establishing inclusion results in the general case. Furthermore we show that some inclusions are strict with unrestricted intervals even when nets are bounded. Then we focus on bounded TPNs with upper-closed intervals and we prove that the semantics are equivalent. Finally taking into account both the practical and the theoretical issues, we conclude that persistent atomic semantics should be preferred.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient On-the-Fly Algorithms for the Analysis of Timed Games.\n \n \n \n \n\n\n \n Cassez, F.; David, A.; Fleury, E.; Larsen, K. G.; and Lime, D.\n\n\n \n\n\n\n In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653, of Lecture Notes in Computer Science, pages 66–80, 2005. Springer\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n \n \"EfficientSlides\n  \n \n \n \"Efficient link\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 1 download\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/concur/CassezDFLL05,\n  author    = {Franck Cassez and\n               Alexandre David and\n               Emmanuel Fleury and\n               Kim Guldstrand Larsen and\n               Didier Lime},\n  title     = {Efficient On-the-Fly Algorithms for the Analysis of Timed Games},\n  booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,\n               {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},\n  pages     = {66--80},\n  year      = {2005},\n          Type = {B - International Conferences},\n\n    series    = {Lecture Notes in Computer Science},\n  volume    = {3653},\n  publisher = {Springer},\n  urlpaper = {papers/efficient-control-concur05.pdf},\n  urlslides = {papers/efficient-control-concur05-slides.pdf},\n  url_link       = {http://dx.doi.org/10.1007/11539452_9},\n  doi       = {10.1007/11539452_9},\n  abstract = {In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties.\nThe algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu &amp; Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.\nVarious optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.},\n  keywords = {control, synthesis, timed games},\n}\n\n\n\n
\n
\n\n\n
\n In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modal Logics for Timed Control.\n \n \n \n \n\n\n \n Bouyer, P.; Cassez, F.; and Laroussinie, F.\n\n\n \n\n\n\n In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653, of Lecture Notes in Computer Science, pages 81–94, 2005. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ModalPaper\n  \n \n \n \"ModalSlides\n  \n \n \n \"Modal link\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/concur/BouyerCL05,\n  author    = {Patricia Bouyer and\n               Franck Cassez and\n               Fran{\\c{c}}ois Laroussinie},\n  title     = {Modal Logics for Timed Control},\n  booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,\n               {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},\n  pages     = {81--94},\n  year      = {2005},\n  crossref  = {DBLP:conf/concur/2005},\n          Type = {B - International Conferences},\n\n  urlpaper = {papers/modal-control-concur05.pdf},\n  urlslides = {papers/slides-concur-05.pdf},\n    url_link       = {http://dx.doi.org/10.1007/11539452_10},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {3653},\n  publisher = {Springer},\n  doi       = {10.1007/11539452_10},\n  abstract = {\nAbstract. In this paper we use the timed modal logic Lnu to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lcont) of the logic Lnu with a new modality.\nMore precisely we define a fragment of Lnu, namely Ldet, such that any\ncontrol objective of Lnudet can be translated into a Lcont formula that\nholds for the plant if and only if there is a controller that can enforce\nthe control objective.\nWe also show that the new modality of Lcont strictly increases the expressive power of Lnu\nwhile model-checking of Lcont remains EXPTIME-complete.},\n  keywords = {control, synthesis, logics},\n}\n\n\n\n
\n
\n\n\n
\n Abstract. In this paper we use the timed modal logic Lnu to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lcont) of the logic Lnu with a new modality. More precisely we define a fragment of Lnu, namely Ldet, such that any control objective of Lnudet can be translated into a Lcont formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of Lcont strictly increases the expressive power of Lnu while model-checking of Lcont remains EXPTIME-complete.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Comparison of the Expressiveness of Timed Automata and Time Petri Nets.\n \n \n \n \n\n\n \n Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n In Pettersson, P.; and Yi, W., editor(s), Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, volume 3829, of Lecture Notes in Computer Science, pages 211–225, 2005. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ComparisonPaper\n  \n \n \n \"ComparisonSlides\n  \n \n \n \"Comparison link\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/formats/BerardCHLR05,\n  author    = {B{\\'{e}}atrice B{\\'{e}}rard and\n               Franck Cassez and\n               Serge Haddad and\n               Didier Lime and\n               Olivier H. Roux},\n  title     = {Comparison of the Expressiveness of Timed Automata and Time Petri\n               Nets},\n  booktitle = {Formal Modeling and Analysis of Timed Systems, Third International\n               Conference, {FORMATS} 2005, Uppsala, Sweden, September 26-28, 2005,\n               Proceedings},\n  pages     = {211--225},\n  editor    = {Paul Pettersson and\n               Wang Yi},\n          Type = {B - International Conferences},\n\n series    = {Lecture Notes in Computer Science},\n  volume    = {3829},\n  publisher = {Springer},\n  year      = {2005},\n  urlpaper = {papers/petri-nets-formats05.pdf},\n  urlslides = {papers/slides-formats-05.pdf},\n  url_link       = {http://dx.doi.org/10.1007/11603009_17},\n  doi       = {10.1007/11603009_17},\n  abstract = { In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur \\&amp; Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA A s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to A. We then propose a structural translation from TA to (1-safe) TPNs preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass bounded and 1-safe TPNs “`a la Merlin” are equally expressive w.r.t. timed bisimilarity.},\n  keywords = {Petri nets, timed automata, expressiveness},\n}\n\n\n\n
\n
\n\n\n
\n In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA A s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to A. We then propose a structural translation from TA to (1-safe) TPNs preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass bounded and 1-safe TPNs “`a la Merlin” are equally expressive w.r.t. timed bisimilarity.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?.\n \n \n \n \n\n\n \n Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; and Roux, O. H.\n\n\n \n\n\n\n In Ramanujam, R.; and Sen, S., editor(s), FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15-18, 2005, Proceedings, volume 3821, of Lecture Notes in Computer Science, pages 273–284, 2005. Springer\n \n\n\n\n
\n\n\n\n \n \n \"WhenPaper\n  \n \n \n \"When link\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/fsttcs/BerardCHLR05,\n  author    = {B{\\'{e}}atrice B{\\'{e}}rard and\n               Franck Cassez and\n               Serge Haddad and\n               Didier Lime and\n               Olivier H. Roux},\n        Type = {B - International Conferences},\n\n  title     = {When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?},\n  booktitle = {{FSTTCS} 2005: Foundations of Software Technology and Theoretical\n               Computer Science, 25th International Conference, Hyderabad, India,\n               December 15-18, 2005, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {3821},\n  publisher = {Springer},\n  editor    = {Ramaswamy Ramanujam and\n               Sandeep Sen},\n  pages     = {273--284},\n  year      = {2005},\n  urlpaper = {papers/petri-nets-fsttcs05.pdf},\n  url_link       = {http://dx.doi.org/10.1007/11590156_22},\n  doi       = {10.1007/11590156_22},\n  abstract = {In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass T  of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for T  are PSPACE-complete. Furthermore we show that for a TA in T  with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.},\n  keywords = {Petri nets, timed automata, bisimulation},\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass T of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for T are PSPACE-complete. Furthermore we show that for a TA in T with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Introduction au contrôle des systèmes temps-réel.\n \n \n \n \n\n\n \n Altisen, K.; Bouyer, P.; Cachat, T.; Cassez, F.; and Gardey, G.\n\n\n \n\n\n\n European Journal of Automated Systems, 39(1-2-3): 367-380. 2005.\n From Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05)\n\n\n\n
\n\n\n\n \n \n \"IntroductionPaper\n  \n \n \n \"IntroductionSlides\n  \n \n \n \"Introduction 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\n
\n
@ARTICLE{Cortos-MSR05-control-journal,\n  AUTHOR = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and Cassez, Franck and Gardey, Guillaume},\n  JOURNAL = {European Journal of Automated Systems},\n  PAGES = {367-380},\n  VOLUME = {39},\n  NUMBER = {1-2-3},\n  Type = {A - Journal},\n  PUBLISHER = {Herm{\\`e}s},\n  TITLE = {Introduction au contrôle des syst{\\`e}mes temps-r{\\'e}el},\n  urlpaper = {papers/intro-control-msr05.pdf},\n  urlslides ={papers/slides-msr05.pdf},\n  url_link = {http://www.lsv.ens-cachan.fr/aci-cortos},\n  YEAR = {2005},\n  note =  {From {A}ctes du 5{\\`e}me {C}olloque sur la {M}od{\\'e}lisation des {S}yst{\\`e}mes {R}{\\'e}actifs ({MSR}'05)},\n  abstract = { In this paper we give a quick overview of the area of control of real-time systems.},\n  keywords = {control, synthesis, timed games},\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2004\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n\n
\n
\n\n\n
\n In this paper we give a quick overview of the area of control of real-time systems.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Synthesis of Optimal Strategies Using HyTech.\n \n \n \n \n\n\n \n Bouyer, P.; Cassez, F.; Fleury, E.; and Larsen, K. G.\n\n\n \n\n\n\n Electr. Notes Theor. Comput. Sci. (Proceedings of GDV), 119(1): 11–31. 2004.\n \n\n\n\n
\n\n\n\n \n \n \"SynthesisPaper\n  \n \n \n \"SynthesisSlides\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\n
\n
@article{DBLP:journals/entcs/BouyerCFL05,\n  author    = {Patricia Bouyer and\n               Franck Cassez and\n               Emmanuel Fleury and\n               Kim Guldstrand Larsen},\n  title     = {Synthesis of Optimal Strategies Using HyTech},\n  journal   = {Electr. Notes Theor. Comput. Sci. (Proceedings of GDV)},\n  volume    = {119},\n  Type = {B - International Conferences},\n\n  number    = {1},\n  pages     = {11--31},\n  year      = {2004},\n  url       = {http://dx.doi.org/10.1016/j.entcs.2004.07.006},\n  urlslides = {papers/slides-gdv-04.pdf},\n  doi       = {10.1016/j.entcs.2004.07.006},\n  abstract = {Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.},\n  keywords = {control, synthesis, priced timed games, optimal},\n}\n\n\n\n
\n
\n\n\n
\n Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Timed Extension for ALTARICA.\n \n \n \n \n\n\n \n Cassez, F.; Pagetti, C.; and Roux, O. H.\n\n\n \n\n\n\n Fundam. Inform., 62(3-4): 291–332. 2004.\n \n\n\n\n
\n\n\n\n \n \n \"APapser\n  \n \n \n \"A link\n  \n \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\n\n\n
\n
@article{DBLP:journals/fuin/CassezPR04,\n  author    = {Franck Cassez and\n               Claire Pagetti and\n               Olivier H. Roux},\n  title     = {A Timed Extension for {ALTARICA}},\n  journal   = {Fundam. Inform.},\n  volume    = {62},\n  number    = {3-4},\n  pages     = {291--332},\n  year      = {2004},\n  urlpapser = {papers/fi-2004.pdf},\n  url_link       = {http://content.iospress.com/articles/fundamenta-informaticae/fi62-3-4-02},\n  ABSTRACT = {  In this paper we present a \\emph{timed} extension of the AltaRica\n  formalism.  Following previous works, we first extend the semantics of\n  AltaRica with time and define \\emph{timed components} and \\emph{timed nodes}.\n  Moreover we lift the \\emph{priority features} of AltaRica to the timed\n  case.  We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give\n  a translation of a Timed AltaRica specification into a usual timed automaton.\n  These are the semantic foundations of a high-level hierarchical\n  language for the specification of timed systems.\n},\n Type = {A - Journal},\n keywords = {timed automata, semantics},\n abstract = {},\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Optimal Strategies in Priced Timed Game Automata.\n \n \n \n \n\n\n \n Bouyer, P.; Cassez, F.; Fleury, E.; and Larsen, K. G.\n\n\n \n\n\n\n In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328, of Lecture Notes in Computer Science, pages 148–160, 2004. Springer\n \n\n\n\n
\n\n\n\n \n \n \"OptimalPaper\n  \n \n \n \"Optimal link\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/fsttcs/BouyerCFL04,\n  author    = {Patricia Bouyer and\n               Franck Cassez and\n               Emmanuel Fleury and\n               Kim Guldstrand Larsen},\n  title     = {Optimal Strategies in Priced Timed Game Automata},\n  booktitle = {{FSTTCS} 2004: Foundations of Software Technology and Theoretical\n               Computer Science, 24th International Conference, Chennai, India, December   16-18, 2004, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {3328},\n  publisher = {Springer},\n\n  pages     = {148--160},\n  year      = {2004},\n  urlpaper = {papers/fsttcs04.pdf},\n  url_link       = {http://dx.doi.org/10.1007/978-3-540-30538-5_13},\n  doi       = {10.1007/978-3-540-30538-5_13},\n  Type = {B - International Conferences},\n  keywords = {control, synthesis, timed games},\n  abstract = {Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost and we prove that it is decidable. Under stronger conditions (strictness of constraints) we prove that in case an optimal strategy exists, we can compute a state-based winning optimal strategy.}\n}\n\n\n\n\n
\n
\n\n\n
\n Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost and we prove that it is decidable. Under stronger conditions (strictness of constraints) we prove that in case an optimal strategy exists, we can compute a state-based winning optimal strategy.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Optimal Strategies in Priced Timed Game Automata.\n \n \n \n \n\n\n \n Bouyer, P.; Cassez, F.; Fleury, E.; and Larsen, K. G.\n\n\n \n\n\n\n Technical Report RS-04-0, BRICS, Denmark, 2004.\n ISSN 0909-0878\n\n\n\n
\n\n\n\n \n \n \"OptimalPaper\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
@TECHREPORT{bouyer-brics-04,\n  ABSTRACT = {  Priced timed (game) automata extends timed (game) automata with costs on both locations and transitions. In this paper we focus on\n  reachability games for priced timed game automata and prove that the\n  optimal cost for winning such a game is computable under conditions\n  concerning the\n  non-zenoness of cost. Under stronger conditions (strictness of\n  constraints) we prove in addition that it is decidable whether there\n  is an optimal strategy in which case an optimal strategy can be\n  computed. Our results extend previous decidability result which\n  requires the underlying game automata to be acyclic. Finally, our\n  results are encoded in a first prototype in {\\em HyTech} which is applied\n  on a small case-study.},\n  AUTHOR = {Bouyer, Patricia and Cassez, Franck and Fleury, Emmanuel and Larsen, Kim Guldstrand},\n  INSTITUTION = {BRICS, Denmark},\n  LEX = {Da},\n  XXMONTH = FEB,\n  NOTE = {ISSN 0909-0878},\n  CATEGORY = {control},\n  NUMBER = {RS-04-0},\n  TITLE = {{Optimal Strategies in Priced Timed Game Automata}},\n  TYPE = {E - Reports},\n  URL = {http://www.brics.dk/RS/04/4/},\n  YEAR = {2004},\n\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2003\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n\n
\n
\n\n\n
\n Priced timed (game) automata extends timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove in addition that it is decidable whether there is an optimal strategy in which case an optimal strategy can be computed. Our results extend previous decidability result which requires the underlying game automata to be acyclic. Finally, our results are encoded in a first prototype in \\em HyTech which is applied on a small case-study.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Hierarchical Modeling and Verification of Timed Systems in Timed AltaRica.\n \n \n \n \n\n\n \n Pagetti, C.; Cassez, F.; and Roux, O.\n\n\n \n\n\n\n In Formal Aspects of Component Software (FACS'03), pages 63–80, September 2003. UNU/IIST, Macau\n Pisa, Italy, September 8–9, 2003\n\n\n\n
\n\n\n\n \n \n \"HierarchicalPaper\n  \n \n \n \"Hierarchical 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\n
\n
@INPROCEEDINGS{pagetti-facs-2003,\n  ABSTRACT = { In this paper we present a timed extension of the AltaRica language,\n  Timed AltaRica, and describe the architecture of a compiler from Timed AltaRica to timed\n  automata. We present the features of the language, namely\n  modularity, hierarchical modeling and reuse of components during the\n  specification phase, on an  avionics example. Then, we use the\n  compiler from Timed AltaRica to Timed Automata to check some safety properties\n  on the system.},\n  AUTHOR = {Pagetti, Claire and Cassez, Franck and Roux, {Olivier F.}},\n  BOOKTITLE = {Formal Aspects of Component Software (FACS'03)},\n  MONTH = SEP,\n  NOTE = {Pisa, Italy, September 8--9, 2003},\n  PAGES = {63--80},\n  PDF = {papers/facs-03.pdf},\n  PUBLISHER = {UNU/IIST, Macau},\n  TITLE = {{Hierarchical Modeling and Verification of Timed Systems in Timed {AltaRica}}},\n  urlpaper = {papers/facs-03.pdf},\n  url_link = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report284.html},\n  YEAR = {2003},\n  Type = {B - International Conferences},\n  keywords = {timed automata, semantics, components},\n}\n\n\n\n\n
\n
\n\n\n
\n In this paper we present a timed extension of the AltaRica language, Timed AltaRica, and describe the architecture of a compiler from Timed AltaRica to timed automata. We present the features of the language, namely modularity, hierarchical modeling and reuse of components during the specification phase, on an avionics example. Then, we use the compiler from Timed AltaRica to Timed Automata to check some safety properties on the system.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Time Petri Nets to Timed Automata.\n \n \n \n \n\n\n \n Cassez, F.; and Roux, O.\n\n\n \n\n\n\n In 4$ème}$ Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'03), 2003. \n \n\n\n\n
\n\n\n\n \n \n \"FromPaper\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
@INPROCEEDINGS{msr-03,\n  AUTHOR = {Cassez, Franck and Roux, {Olivier H.}},\n  BOOKTITLE = {4$\\textit{\\`eme}$ Colloque Francophone sur la Mod{\\'e}lisation des Syst{\\`e}mes R{\\'e}actifs, (MSR'03)},\n  urlpaper = {papers/ri-msr-03.pdf},\n  TITLE = {{From Time Petri Nets to Timed Automata}},\n  YEAR = {2003},\n  ABSTRACT = {\n In this paper, we consider Time Petri Nets (TPN) where time is\n  associated with transitions. We give a formal semantics for TPNs in\n  terms of Timed Transition Systems.  Then, we propose a translation\n  from TPNs to Timed Automata (TA) that preserves the behavioural\n  semantics (timed bisimilarity) of the TPNs.  For the theory of TPNs\n  this result is two-fold: i) reachability problems and more generally\n  TCTL model-checking are decidable for bounded TPNs; ii) allowing\n  strict time constraints on transitions for TPNs preserves the\n  results described in i).  The practical applications of the\n  translation are: i) one can specify a system using both TPNs and\n  Timed Automata and a precise semantics is given to the composition;\n  ii) one can use existing tools for analysing timed automata (like\n  KRONOS or UPPAAL or CMC) to analyse TPNs.\n},\n  Type = {B - International Conferences}\n}\n\n
\n
\n\n\n
\n In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like KRONOS or UPPAAL or CMC) to analyse TPNs. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Vérification qualitative – Model-Checking et Logiques Temporelles.\n \n \n \n \n\n\n \n Cassez, F.\n\n\n \n\n\n\n Actes de l'école d'été ETR'03, 2003.\n \n\n\n\n
\n\n\n\n \n \n \"VérificationPaper\n  \n \n \n \"VérificationSlides\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-etr-03,\n  AUTHOR = {Cassez, Franck},\n  HOWPUBLISHED = {Actes de l'\\'ecole d'\\'et\\'e ETR'03},\n  XXMONTH = SEP,\n  urlpaper = {papers/verif-qualit-etr-03.pdf},\n  urlslides = {papers/slides-etr-03.pdf},\n  keywords = {verification, logics},\n  TITLE = {{V\\'erification qualitative -- {Model-Checking} et Logiques Temporelles}},\n  YEAR = {2003},\nabstract = {In this paper we give a quick overview of the area of modelling and verification of concurrent systems. We take transition systems as the basic model of concurrent systems, and introduce the temporal logics LTL and CTL. Moreover we give some hints for the model-checking algorithms for LTL and CTL.},\nType = {E - Reports},\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2002\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n\n
\n
\n\n\n
\n In this paper we give a quick overview of the area of modelling and verification of concurrent systems. We take transition systems as the basic model of concurrent systems, and introduce the temporal logics LTL and CTL. Moreover we give some hints for the model-checking algorithms for LTL and CTL.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The Impressive Power of Stopwatches.\n \n \n \n \n\n\n \n Cassez, F.; and Larsen, K. G.\n\n\n \n\n\n\n In Palamidessi, C., editor(s), CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877, of Lecture Notes in Computer Science, pages 138–152, 2000. Springer\n CONCUR Test-Of-Time Award 2022\n\n\n\n
\n\n\n\n \n \n \"ThePaper\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 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/concur/CassezL00,\n  author    = {Franck Cassez and\n               Kim Guldstrand Larsen},\n  editor    = {Catuscia Palamidessi},\n  title     = {The Impressive Power of Stopwatches},\n  booktitle = {{CONCUR} 2000 - Concurrency Theory, 11th International Conference,\n               University Park, PA, USA, August 22-25, 2000, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {1877},\n  pages     = {138--152},\n  publisher = {Springer},\n  year      = {2000},\n  url       = {https://doi.org/10.1007/3-540-44618-4\\_12},\n  doi       = {10.1007/3-540-44618-4\\_12},\n  timestamp = {Tue, 14 May 2019 10:00:43 +0200},\n  urlpaper = {papers/concur-00.pdf},\n  biburl    = {https://dblp.org/rec/conf/concur/CassezL00.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note      = {CONCUR Test-Of-Time Award 2022}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1998\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Effective Recognizability and Model Checking of Reactive FIFFO Automata.\n \n \n \n \n\n\n \n Sutre, G.; Finkel, A.; Roux, O.; and Cassez, F.\n\n\n \n\n\n\n In Algebraic Methodology and Software Technology, 7th International Conference, AMAST '98, pages 106-123, 1998. \n \n\n\n\n
\n\n\n\n \n \n \"EffectiveLink\n  \n \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{amast-98,\n  author    = {Sutre, Grégoire  and\n                Finkel, Alain and\n                Roux, {Olivier F.} and\n                Cassez, Franck},\n  title     = {Effective Recognizability and Model Checking of Reactive\n               {FIFFO} Automata},\n  booktitle = {Algebraic Methodology and Software Technology, 7th International\n               Conference, AMAST '98},\n  year      = {1998},\n  pages     = {106-123},\n  ee        = {http://dx.doi.org/10.1007/3-540-49253-4_10},\n  crossref  = {DBLP:conf/amast/1998},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  Type = {B - International Conferences},\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\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);