var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\",\"jsonp\":\"1\",\"filter\":\"keywords:wcet\",\"css\":\"true\",\"host\":\"bibbase.org\"},\n      data: [{\"bibtype\":\"article\",\"type\":\"A - Journal\",\"title\":\"Efficient and Scalable Runtime Monitoring for Cyber–Physical System\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Zheng\"],\"firstnames\":[\"Xi\"],\"suffixes\":[]},{\"firstnames\":[\"Christine\"],\"propositions\":[],\"lastnames\":[\"Julien\"],\"suffixes\":[]},{\"firstnames\":[\"Rodion M.\"],\"propositions\":[],\"lastnames\":[\"Podorozhny\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Thierry\"],\"propositions\":[],\"lastnames\":[\"Rakotoarivelo\"],\"suffixes\":[]}],\"journal\":\"IEEE Systems Journal\",\"year\":\"2016\",\"volume\":\"99\",\"pages\":\"1–12\",\"publisher\":\"IEEE\",\"doi\":\"10.1109/JSYST.2016.2614599\",\"issn\":\"1932-8184\",\"urlpaper\":\"papers/ieee-systems-2016.pdf\",\"url_link\":\"http://ieeexplore.ieee.org/document/7605519/\",\"month\":\"October\",\"show\":\"\",\"keywords\":\"wcet, timed automata\",\"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.\",\"bibtex\":\"@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\",\"author_short\":[\"Zheng, X.\",\"Julien, C.\",\"Podorozhny, R.\",\"Cassez, F.\",\"Rakotoarivelo, T.\"],\"key\":\"ieee-16\",\"id\":\"ieee-16\",\"bibbaseid\":\"zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/ieee-systems-2016.pdf\",\" link\":\"http://ieeexplore.ieee.org/document/7605519/\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Xi\"],\"propositions\":[],\"lastnames\":[\"Zheng\"],\"suffixes\":[]},{\"firstnames\":[\"Christine\"],\"propositions\":[],\"lastnames\":[\"Julien\"],\"suffixes\":[]},{\"firstnames\":[\"Rodion M.\"],\"propositions\":[],\"lastnames\":[\"Podorozhny\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]}],\"title\":\"BraceAssertion: Runtime Verification of Cyber-Physical Systems\",\"booktitle\":\"12th IEEE International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015, Dallas, TX, USA, October 19-22, 2015\",\"pages\":\"298–306\",\"year\":\"2015\",\"urlpaper\":\"papers/mass-2015.pdf\",\"url_link\":\"http://dx.doi.org/10.1109/MASS.2015.15\",\"doi\":\"10.1109/MASS.2015.15\",\"timestamp\":\"Fri, 06 May 2016 13:36:43 +0200\",\"biburl\":\"http://dblp.uni-trier.de/rec/bib/conf/mass/ZhengJPC15\",\"bibsource\":\"dblp computer science bibliography, http://dblp.org\",\"show\":\"\",\"keywords\":\"wcet, timed automata\",\"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.\",\"bibtex\":\"@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\",\"author_short\":[\"Zheng, X.\",\"Julien, C.\",\"Podorozhny, R.\",\"Cassez, F.\"],\"key\":\"mass-Zheng-15\",\"id\":\"mass-Zheng-15\",\"bibbaseid\":\"zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/mass-2015.pdf\",\" link\":\"http://dx.doi.org/10.1109/MASS.2015.15\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Pablo\",\"González\"],\"propositions\":[\"de\"],\"lastnames\":[\"Aledo\",\"Marugán\"],\"suffixes\":[]}],\"title\":\"Timed Automata for Modelling Caches and Pipelines\",\"booktitle\":\"Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, November 23, 2015.\",\"pages\":\"37–45\",\"year\":\"2015\",\"editor\":[{\"firstnames\":[\"Rob\",\"J.\"],\"propositions\":[\"van\"],\"lastnames\":[\"Glabbeek\"],\"suffixes\":[]},{\"firstnames\":[\"Jan\",\"Friso\"],\"propositions\":[],\"lastnames\":[\"Groote\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\"],\"propositions\":[],\"lastnames\":[\"Höfner\"],\"suffixes\":[]}],\"series\":\"EPTCS\",\"volume\":\"196\",\"url_link\":\"http://dx.doi.org/10.4204/EPTCS.196.4\",\"urlslides\":\"papers/slides-mars-2015.pdf\",\"doi\":\"10.4204/EPTCS.196.4\",\"category\":\"wcet\",\"mywebpage\":\"wcet\",\"show\":\"\",\"keywords\":\"wcet, timed automata\",\"abstract\":\"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. \",\"bibtex\":\"@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\",\"author_short\":[\"Cassez, F.\",\"de Aledo Marugán, P. G.\"],\"editor_short\":[\"van Glabbeek, R. J.\",\"Groote, J. F.\",\"Höfner, P.\"],\"key\":\"cassez-mars-2015\",\"id\":\"cassez-mars-2015\",\"bibbaseid\":\"cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015\",\"role\":\"author\",\"urls\":{\" link\":\"http://dx.doi.org/10.4204/EPTCS.196.4\",\"Slides\":\"http://science.mq.edu.au/~fcassez/bib/papers/slides-mars-2015.pdf\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Jean-Luc\"],\"propositions\":[],\"lastnames\":[\"Béchennec\"],\"suffixes\":[]}],\"title\":\"Timing Analysis of Binary Programs with UPPAAL\",\"booktitle\":\"13th International Conference on Application of Concurrency to System Design, ACSD 2013\",\"year\":\"2013\",\"month\":\"July\",\"pages\":\"41-50\",\"publisher\":\"IEEE Computer Society\",\"urlpaper\":\"papers/acsd-2013.pdf\",\"urlslides\":\"papers/slides-acsd-wcet-2013.pdf\",\"doi\":\"http://dx.doi.org/10.1109/ACSD.2013.7\",\"mywebpage\":\"wcet\",\"show\":\"\",\"keywords\":\"wcet, timed automata\",\"abstract\":\"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. \",\"bibtex\":\"@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\",\"author_short\":[\"Cassez, F.\",\"Béchennec, J.\"],\"key\":\"cassez-acsd-13\",\"id\":\"cassez-acsd-13\",\"bibbaseid\":\"cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2013.pdf\",\"Slides\":\"http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-wcet-2013.pdf\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"downloads\":3,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"René\",\"Rydhof\"],\"propositions\":[],\"lastnames\":[\"Hansen\"],\"suffixes\":[]},{\"firstnames\":[\"Mads\",\"Chr.\"],\"propositions\":[],\"lastnames\":[\"Olesen\"],\"suffixes\":[]}],\"title\":\"What is a Timing Anomaly?\",\"booktitle\":\"12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy\",\"year\":\"2012\",\"pages\":\"1-12\",\"urlpaper\":\"papers/wcet-2012.pdf\",\"url_link\":\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\",\"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.\",\"category\":\"wcet\",\"mywebpage\":\"soft-verif,wcet\",\"keywords\":\"wcet\",\"publisher\":\"Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik\",\"series\":\"OASICS\",\"volume\":\"23\",\"bibtex\":\"@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\",\"author_short\":[\"Cassez, F.\",\"Hansen, R. R.\",\"Olesen, M. C.\"],\"key\":\"wcet-12\",\"id\":\"wcet-12\",\"bibbaseid\":\"cassez-hansen-olesen-whatisatiminganomaly-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\",\" link\":\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\"},\"keyword\":[\"wcet\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]}],\"title\":\"Timed Games for Computing WCET for Pipelined Processors with Caches\",\"booktitle\":\"11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011\",\"pages\":\"195–204\",\"year\":\"2011\",\"publisher\":\"IEEE\",\"url\":\"http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.15\",\"doi\":\"10.1109/ACSD.2011.15\",\"timestamp\":\"Wed, 15 Feb 2012 09:59:43 +0100\",\"biburl\":\"http://dblp.uni-trier.de/rec/bib/conf/acsd/Cassez11\",\"bibsource\":\"dblp computer science bibliography, http://dblp.org\",\"urlpaper\":\"papers/acsd-2011.pdf\",\"urlslides\":\"papers/slides-acsd-2011.pdf\",\"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. \",\"ee\":\"http://dx.doi.org/10.1109/ACSD.2011.15\",\"keywords\":\"wcet, timed automata\",\"category\":\"wcet\",\"show\":\"\",\"mywebpage\":\"wcet\",\"bibtex\":\"@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\",\"author_short\":[\"Cassez, F.\"],\"key\":\"cassez-acsd-2011\",\"id\":\"cassez-acsd-2011\",\"bibbaseid\":\"cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf\",\"Slides\":\"http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-2011.pdf\",\"Link\":\"http://dx.doi.org/10.1109/ACSD.2011.15\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"E - Reports\",\"author\":[{\"firstnames\":[\"Jean-Luc\"],\"propositions\":[],\"lastnames\":[\"Béchennec\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]}],\"title\":\"Computation of WCET using Program Slicing and Real-Time Model-Checking\",\"journal\":\"CoRR\",\"volume\":\"abs/1105.1633\",\"year\":\"2011\",\"urlpaper\":\"http://arxiv.org/abs/1105.1633\",\"timestamp\":\"Mon, 05 Dec 2011 18:05:32 +0100\",\"biburl\":\"http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1105-1633\",\"bibsource\":\"dblp computer science bibliography, http://dblp.org\",\"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.\",\"category\":\"wcet\",\"keywords\":\"wcet, timed automata\",\"show\":\"\",\"mywebpage\":\"wcet\",\"bibtex\":\"@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\",\"author_short\":[\"Béchennec, J.\",\"Cassez, F.\"],\"key\":\"bech-wcet-2011\",\"id\":\"bech-wcet-2011\",\"bibbaseid\":\"bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://arxiv.org/abs/1105.1633\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"E - Reports\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]}],\"title\":\"Timed Games for Computing Worst-Case Execution-Times\",\"journal\":\"CoRR\",\"volume\":\"abs/1006.1951\",\"year\":\"2010\",\"url\":\"http://arxiv.org/abs/1006.1951\",\"timestamp\":\"Mon, 05 Dec 2011 18:04:54 +0100\",\"biburl\":\"http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1006-1951\",\"bibsource\":\"dblp computer science bibliography, http://dblp.org\",\"keywords\":\"wcet, timed automata\",\"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.\",\"bibtex\":\"@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\",\"author_short\":[\"Cassez, F.\"],\"key\":\"DBLP:journals/corr/abs-1006-1951\",\"id\":\"DBLP:journals/corr/abs-1006-1951\",\"bibbaseid\":\"cassez-timedgamesforcomputingworstcaseexecutiontimes-2010\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://arxiv.org/abs/1006.1951\"},\"keyword\":[\"wcet\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"}],\n      metadata: {\"owner\":\"cassez, f\",\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\n      ownerID: \"aYsqprsgp7HA5GpQ3\"\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"franck-bib.bib\" href=\"data:text/bibtex;base64,QGFydGljbGV7aWVlZS0xNiwKICB0aXRsZT17RWZmaWNpZW50IGFuZCBTY2FsYWJsZSBSdW50aW1lIE1vbml0b3JpbmcgZm9yIEN5YmVyLS1QaHlzaWNhbCBTeXN0ZW19LAogIGF1dGhvcj17WmhlbmcsIFhpIGFuZCBDaHJpc3RpbmUgSnVsaWVuIGFuZCB7Um9kaW9uIE0ufSBQb2Rvcm96aG55ICBhbmQgRnJhbmNrIENhc3NleiBhbmQgVGhpZXJyeSBSYWtvdG9hcml2ZWxvfSwKICBqb3VybmFsPXtJRUVFIFN5c3RlbXMgSm91cm5hbH0sCiAgeWVhcj17MjAxNn0sCiAgdm9sdW1lPTk5LAogIHBhZ2VzPXsxLS0xMn0sCiAgcHVibGlzaGVyPXtJRUVFfSwKICBkb2k9ezEwLjExMDkvSlNZU1QuMjAxNi4yNjE0NTk5fSwKICBJU1NOPXsxOTMyLTgxODR9LAogIHVybHBhcGVyPXtwYXBlcnMvaWVlZS1zeXN0ZW1zLTIwMTYucGRmfSwKICB1cmxfbGluaz17aHR0cDovL2llZWV4cGxvcmUuaWVlZS5vcmcvZG9jdW1lbnQvNzYwNTUxOS99LAogIG1vbnRoPW9jdCwKICBzaG93ID0ge30sCiAga2V5d29yZHMgPSB7d2NldCwgdGltZWQgYXV0b21hdGF9LAoKICBhYnN0cmFjdD17T3VyIHJlbGlhbmNlIG9uIGN5YmVy4oCTcGh5c2ljYWwgc3lzdGVtcyAoQ1BTcykgaXMgaW5jcmVhc2luZ2x5IHdpZGVzcHJlYWQsIGJ1dCBzY2FsYWJsZSBtZXRob2RzIGZvciB0aGUgYW5hbHlzaXMgb2Ygc3VjaCBzeXN0ZW1zIHJlbWFpbiBhIHNpZ25pZmljYW50IGNoYWxsZW5nZS4gUnVudGltZSB2ZXJpZmljYXRpb24gb2YgQ1BTcyBwcm92aWRlcyBhIHJlYXNvbmFibGUgbWlkZGxlIGdyb3VuZCBiZXR3ZWVuIGZvcm1hbCB2ZXJpZmljYXRpb24gYW5kIHNpbXVsYXRpb24gYXBwcm9hY2hlcywgYnV0IGl0IGNvbWVzIHdpdGggaXRzIG93biBjaGFsbGVuZ2VzLiBBIHJ1bnRpbWUgdmVyaWZpY2F0aW9uIHN5c3RlbSBtdXN0IHJ1biBkaXJlY3RseSBvbiB0aGUgZGVwbG95ZWQgYXBwbGljYXRpb24uIEluIHRoZSBDUFMgZG9tYWluLCBpdCBpcyB0aGVyZWZvcmUgY3JpdGljYWwgdGhhdCBhIHJ1bnRpbWUgdmVyaWZpY2F0aW9uIHN5c3RlbSBleGhpYml0cyBsb3cgb3ZlcmhlYWQgYW5kIGdvb2Qgc2NhbGFiaWxpdHkgc28gdGhhdCB0aGUgdmVyaWZpY2F0aW9uIGRvZXMgbm90IGludGVyZmVyZSB3aXRoIHRoZSBhbmFseXplZCBDUFMgYXBwbGljYXRpb24uIEluIHRoaXMgcGFwZXIsIHdlIGludHJvZHVjZSBCcmFjZSwgYSBydW50aW1lIHZlcmlmaWNhdGlvbiBzeXN0ZW0gd2hvc2UgZm9jdXMgaXMgb24gZW5zdXJpbmcgdGhlc2UgcGVyZm9ybWFuY2UgcXVhbGl0aWVzIGZvciBhcHBsaWNhdGlvbnMgaW4gdGhlIENQUyBkb21haW4uIEJyYWNlIHN0cml2ZXMgdG8gYm91bmQgdGhlIGNvbXB1dGF0aW9uIG92ZXJoZWFkIGZvciBDUFMgcnVudGltZSB2ZXJpZmljYXRpb24gd2hpbGUgcHJlc2VydmluZyBhIGhpZ2ggbGV2ZWwgb2YgbW9uaXRvcmluZyBhY2N1cmFjeSBpbiB0ZXJtcyBvZiB0aGUgbnVtYmVyIG9mIGZhbHNlIHBvc2l0aXZlIGFuZCBmYWxzZSBuZWdhdGl2ZSByZXBvcnRzLiBCcmFjZSBpcyBwYXJ0aWN1bGFybHkgc3VpdGFibGUgdG8gc3lzdGVtcyBpbiB3aGljaCBzY2hlZHVsaW5nIGlzIGRpc3RyaWJ1dGVkIGFjcm9zcyBuZXR3b3JrZWQgQ1BTIGNvbXBvbmVudHMuIFdlIGV2YWx1YXRlIEJyYWNlIHRvIGRldGVybWluZSBob3cgZWZmZWN0aXZlbHkgYW5kIGVmZmljaWVudGx5IGl0IGNhbiBkZXRlY3QgaW5qZWN0ZWQgZXJyb3JzIGluIHR3byBleGlzdGluZyByZWFsLWxpZmUgQ1BTIGFwcGxpY2F0aW9ucyB3aXRoIGRpc3RyaWJ1dGVkIHNjaGVkdWxpbmcuIE91ciByZXN1bHRzIGRlbW9uc3RyYXRlIHRoYXQgQnJhY2UgZWZmaWNpZW50bHkgZGV0ZWN0cyB0aG9zZSBlcnJvcnMgYW5kIGEgZmV3IHRydWUgYnVncyBhbmQgaXMgYWJsZSB0byBib3VuZCBib3RoIHRoZSBtZW1vcnkgYW5kIGNvbXB1dGF0aW9uIG92ZXJoZWFkIGV2ZW4gaW4gc3lzdGVtcyB3aXRoIGxhcmdlIG51bWJlcnMgb2Ygb2JzZXJ2ZWQgZXZlbnRzLn0sCiAgVHlwZSA9IHtBIC0gSm91cm5hbH0sCgp9CgoKCkBpbnByb2NlZWRpbmdze21hc3MtWmhlbmctMTUsCiAgYXV0aG9yICAgID0ge1hpIFpoZW5nIGFuZAogICAgICAgICAgICAgICBDaHJpc3RpbmUgSnVsaWVuIGFuZAogICAgICAgICAgICAgICB7Um9kaW9uIE0ufSBQb2Rvcm96aG55IGFuZAogICAgICAgICAgICAgICBGcmFuY2sgQ2Fzc2V6fSwKICB0aXRsZSAgICAgPSB7QnJhY2VBc3NlcnRpb246IFJ1bnRpbWUgVmVyaWZpY2F0aW9uIG9mIEN5YmVyLVBoeXNpY2FsIFN5c3RlbXN9LAogIGJvb2t0aXRsZSA9IHsxMnRoIHtJRUVFfSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gTW9iaWxlIEFkIEhvYyBhbmQgU2Vuc29yIFN5c3RlbXMsCiAgICAgICAgICAgICAgIHtNQVNTfSAyMDE1LCBEYWxsYXMsIFRYLCBVU0EsIE9jdG9iZXIgMTktMjIsIDIwMTV9LAogIHBhZ2VzICAgICA9IHsyOTgtLTMwNn0sCiAgeWVhciAgICAgID0gezIwMTV9LAogIHVybHBhcGVyID0ge3BhcGVycy9tYXNzLTIwMTUucGRmfSwKICB1cmxfbGluayAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMTA5L01BU1MuMjAxNS4xNX0sCiAgZG9pICAgICAgID0gezEwLjExMDkvTUFTUy4yMDE1LjE1fSwKICB0aW1lc3RhbXAgPSB7RnJpLCAwNiBNYXkgMjAxNiAxMzozNjo0MyArMDIwMH0sCiAgYmlidXJsICAgID0ge2h0dHA6Ly9kYmxwLnVuaS10cmllci5kZS9yZWMvYmliL2NvbmYvbWFzcy9aaGVuZ0pQQzE1fSwKICBiaWJzb3VyY2UgPSB7ZGJscCBjb21wdXRlciBzY2llbmNlIGJpYmxpb2dyYXBoeSwgaHR0cDovL2RibHAub3JnfSwKICBzaG93ID0ge30sCiAga2V5d29yZHMgPSB7d2NldCwgdGltZWQgYXV0b21hdGF9LAoKICBhYnN0cmFjdD17Q3liZXItUGh5c2ljYWwgU3lzdGVtcyAoQ1BTKSBoYXZlIGdhaW5lZCB3aWRlIHBvcHVsYXJpdHksIGhvd2V2ZXIsIGRldmVsb3BpbmcgYW5kIGRlYnVnZ2luZyBDUFMgcmVtYWluIHNpZ25pZmljYW50IGNoYWxsZW5nZXMuIE1hbnkgYnVncyBhcmUgZGV0ZWN0YWJsZSBvbmx5IGF0IHJ1bnRpbWUgdW5kZXIgZGVwbG95bWVudCBjb25kaXRpb25zIHRoYXQgbWF5IGJlIHVucHJlZGljdGFibGUgb3IgYXQgbGVhc3QgdW5leHBlY3RlZCBhdCBkZXZlbG9wbWVudCB0aW1lLiBUaGUgY3VycmVudCBzdGF0ZSBvZiB0aGUgcHJhY3RpY2Ugb2YgZGVidWdnaW5nIENQUyBpcyBnZW5lcmFsbHkgYWQgaG9jLCBpbnZvbHZpbmcgdHJpYWwgYW5kIGVycm9yIGluIGEgcmVhbCBkZXBsb3ltZW50LiBGb3IgaW5jcmVhc2VkIHJpZ29yLCBpdCBpcyBhcHBlYWxpbmcgdG8gYnJpbmcgZm9ybWFsIG1ldGhvZHMgdG8gQ1BTIHZlcmlmaWNhdGlvbi4gSG93ZXZlciBkZXZlbG9wZXJzIG9mdGVuIGVzY2hldyBmb3JtYWwgYXBwcm9hY2hlcyBkdWUgdG8gY29tcGxleGl0eSBhbmQgbGFjayBvZiBlZmZpY2llbmN5LiBUaGlzIHBhcGVyIHByZXNlbnRzIEJyYWNlIEFzc2VydGlvbiwgYSBzcGVjaWZpY2F0aW9uIGZyYW1ld29yayBiYXNlZCBvbiBuYXR1cmFsIGxhbmd1YWdlIHF1ZXJpZXMgdGhhdCBhcmUgYXV0b21hdGljYWxseSBjb252ZXJ0ZWQgdG8gYSBkZXRlcm1pbml0aWMgY2xhc3Mgb2YgdGltZWQgYXV0b21hdGEgdXNlZCBmb3IgcnVudGltZSBtb25pdG9yaW5nLiBUbyByZWR1Y2UgcnVudGltZSBvdmVyaGVhZCBhbmQgc3VwcG9ydCBwcm9wZXJ0aWVzIHRoYXQgcmVmZXJlbmNlIHByZWRpY2F0ZSBsb2dpYywgd2UgdXNlIGEgc2Vjb25kIG1vbml0b3IgYXV0b21hdG9uIHRvIGNyZWF0ZSBmaWx0ZXJlZCB0cmFjZXMgb24gd2hpY2ggdG8gcnVuIHRoZSBhbmFseXNpcyB1c2luZyB0aGUgc3BlY2lmaWNhdGlvbiBtb25pdG9yLiBXZSBldmFsdWF0ZSB0aGUgQnJhY2UgQXNzZXJ0aW9uIGZyYW1ld29yayB1c2luZyBhIHJlYWwgQ1BTIGNhc2Ugc3R1ZHkgYW5kIHNob3cgdGhhdCB0aGUgZnJhbWV3b3JrIGlzIGFibGUgdG8gbWluaW1pemUgcnVudGltZSBvdmVyaGVhZCB3aXRoIGFuIGluY3JlYXNpbmcgbnVtYmVyIG9mIG1vbml0b3JzLn0sCiAgVHlwZSA9IHtCIC0gSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlc30sCgp9CgoKCkBpbnByb2NlZWRpbmdze2Nhc3Nlei1tYXJzLTIwMTUsCiAgYXV0aG9yICAgID0ge0ZyYW5jayBDYXNzZXogYW5kCiAgICAgICAgICAgICAgIFBhYmxvIEdvbnp7XCd7YX19bGV6IGRlIEFsZWRvIE1hcnVne1wne2F9fW59LAogIHRpdGxlICAgICA9IHtUaW1lZCBBdXRvbWF0YSBmb3IgTW9kZWxsaW5nIENhY2hlcyBhbmQgUGlwZWxpbmVzfSwKICBib29rdGl0bGUgPSB7UHJvY2VlZGluZ3MgV29ya3Nob3Agb24gTW9kZWxzIGZvciBGb3JtYWwgQW5hbHlzaXMgb2YgUmVhbCBTeXN0ZW1zLAogICAgICAgICAgICAgICB7TUFSU30gMjAxNSwgU3V2YSwgRmlqaSwgTm92ZW1iZXIgMjMsIDIwMTUufSwKICBwYWdlcyAgICAgPSB7MzctLTQ1fSwKICB5ZWFyICAgICAgPSB7MjAxNX0sCiAgIGVkaXRvciAgICA9IHtSb2IgSi4gdmFuIEdsYWJiZWVrIGFuZAogICAgICAgICAgICAgICBKYW4gRnJpc28gR3Jvb3RlIGFuZAogICAgICAgICAgICAgICBQZXRlciBIe1wie299fWZuZXJ9LAogICAgICAgICAgICAgICAgc2VyaWVzICAgID0ge3tFUFRDU319LAogIHZvbHVtZSAgICA9IHsxOTZ9LAogIHllYXIgICAgICA9IHsyMDE1fSwKICB1cmxfbGluayAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC40MjA0L0VQVENTLjE5Ni40fSwKICAgIHVybHNsaWRlcyA9IHtwYXBlcnMvc2xpZGVzLW1hcnMtMjAxNS5wZGZ9LAogIGRvaSAgICAgICA9IHsxMC40MjA0L0VQVENTLjE5Ni40fSwKICBjYXRlZ29yeT0ge3djZXR9LAogIG15d2VicGFnZSA9IHt3Y2V0fSwKICBzaG93ID0ge30sCiAga2V5d29yZHMgPSB7d2NldCwgdGltZWQgYXV0b21hdGF9LAogIGFic3RyYWN0ID0gewogIEluIHRoaXMgcGFwZXIsIHdlIGZvY3VzIG9uIG1vZGVsbGluZyB0aGUgdGltaW5nIGFzcGVjdHMgb2YgYmluYXJ5IHByb2dyYW1zIHJ1bm5pbmcgb24gYXJjaGl0ZWN0dXJlcyBmZWF0dXJpbmcgY2FjaGVzIGFuZCBwaXBlbGluZXMuIFRoZSBvYmplY3RpdmUgaXMgdG8gb2J0YWluIGEgdGltZWQgYXV0b21hdG9uIG1vZGVsIHRvIGNvbXB1dGUgdGlnaHQgYm91bmRzIGZvciB0aGUgd29yc3QtY2FzZSBleGVjdXRpb24gdGltZSAoV0NFVCkgb2YgdGhlIHByb2dyYW1zIHVzaW5nIG1vZGVsLWNoZWNraW5nIHRlY2huaXF1ZXMuCiAgfSwKICBUeXBlID0ge0IgLSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2VzfSwKfQoKCgpAaW5wcm9jZWVkaW5nc3tjYXNzZXotYWNzZC0xMywKICBhdXRob3IgICAgPSB7RnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAge0plYW4tTHVjfSBCw6ljaGVubmVjfSwKICB0aXRsZSAgICAgPSB7VGltaW5nIEFuYWx5c2lzIG9mIEJpbmFyeSBQcm9ncmFtcyB3aXRoIHtVUFBBQUx9fSwKICBib29rdGl0bGUgPSB7MTN0aCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gQXBwbGljYXRpb24gb2YgQ29uY3VycmVuY3kKICAgICAgICAgICAgICAgdG8gU3lzdGVtIERlc2lnbiwgQUNTRCAyMDEzfSwKICB5ZWFyICAgICAgPSB7MjAxM30sCiAgbW9udGggPSBqdWwsCiAgcGFnZXMgICAgID0gezQxLTUwfSwKICAgIFBVQkxJU0hFUiA9IHtJRUVFIENvbXB1dGVyIFNvY2lldHl9LAogIHVybHBhcGVyID0ge3BhcGVycy9hY3NkLTIwMTMucGRmfSwKICB1cmxzbGlkZXMgPSB7cGFwZXJzL3NsaWRlcy1hY3NkLXdjZXQtMjAxMy5wZGZ9LAogIGRvaSAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMTA5L0FDU0QuMjAxMy43fSwKICBteXdlYnBhZ2UgPSB7d2NldH0sCiAgc2hvdyA9IHt9LAogIGtleXdvcmRzID0ge3djZXQsIHRpbWVkIGF1dG9tYXRhfSwKICBhYnN0cmFjdCA9IHsKICBXZSBhZGRyZXNzIHRoZSBwcm9ibGVtIG9mIGNvbXB1dGluZyBhY2N1cmF0ZSBXb3JzdC1DYXNlIEV4ZWN1dGlvbiBUaW1lIChXQ0VUKS4gV2UgcHJvcG9zZSBhIGZ1bGx5IGF1dG9tYXRpYyBhbmQgbW9kdWxhciBtZXRob2RvbG9neSBiYXNlZCBvbiBwcm9ncmFtIHNsaWNpbmcgYW5kIHJlYWwtdGltZSBtb2RlbC1jaGVja2luZy4gV2UgaGF2ZSBpbXBsZW1lbnRlZCBvdXIgbWV0aG9kb2xvZ3kgYW5kIGFwcGxpZWQgaXQgdG8gc3RhbmRhcmQgYmVuY2htYXJrcy4gVG8gZnVydGhlciB2YWxpZGF0ZSB0aGUgYXBwcm9hY2gsIHdlIGFsc28gY29tcGFyZSBvdXIgcmVzdWx0cyB0byB0aGUgcmVhbCBleGVjdXRpb24gdGltZXMgb2YgdGhlIHByb2dyYW1zIG1lYXN1cmVkIG9uIGEgcmVhbCBib2FyZC4KICB9LAogICAgICBUeXBlID0ge0IgLSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2VzfSwKCn0KCiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCiUlJSAyMDEyCiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCgoKCkBpbnByb2NlZWRpbmdze3djZXQtMTIsCiAgYXV0aG9yICAgID0ge0ZyYW5jayBDYXNzZXogYW5kCiAgICAgICAgICAgICAgIFJlbsOpIFJ5ZGhvZiBIYW5zZW4gYW5kCiAgICAgICAgICAgICAgIE1hZHMgQ2hyLiBPbGVzZW59LAogIHRpdGxlICAgICA9IHtXaGF0IGlzIGEgVGltaW5nIEFub21hbHk/fSwKICBib29rdGl0bGUgPSB7MTJ0aCBJbnRlcm5hdGlvbmFsIFdvcmtzaG9wIG9uIFdvcnN0LUNhc2UgRXhlY3V0aW9uIFRpbWUKICAgICAgICAgICAgICAgQW5hbHlzaXMsIFdDRVQgMjAxMiwgSnVseSAxMCwgMjAxMiwgUGlzYSwgSXRhbHl9LAogIHllYXIgICAgICA9IHsyMDEyfSwKICBwYWdlcyAgICAgPSB7MS0xMn0sCiAgdXJscGFwZXIgPSB7cGFwZXJzL3djZXQtMjAxMi5wZGZ9LAogIHVybF9saW5rICAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC40MjMwL09BU0ljcy5XQ0VULjIwMTIuMX0sCiAgYWJzdHJhY3QgPSB7VGltaW5nIGFub21hbGllcyBtYWtlIHdvcnN0LWNhc2UgZXhlY3V0aW9uIHRpbWUgYW5hbHlzaXMgbXVjaCBoYXJkZXIsIGJlY2F1c2UgdGhlIGFuYWx5c2lzIHdpbGwgaGF2ZSB0byBjb25zaWRlciBhbGwgbG9jYWwgY2hvaWNlcy4gSXQgaGFzIGJlZW4gd2lkZWx5IHJlY29nbmlzZWQgdGhhdCBjZXJ0YWluIGhhcmR3YXJlIGZlYXR1cmVzIGFyZSB0aW1pbmcgYW5vbWFsb3VzLCB3aGlsZSBvdGhlcnMgYXJlIG5vdC4gSG93ZXZlciwgZGVmaW5pbmcgZm9ybWFsbHkgd2hhdCBhIHRpbWluZyBhbm9tYWx5IGlzLCBoYXMgYmVlbiBkaWZmaWN1bHQuIFdlIGV4YW1pbmUgcHJldmlvdXMgZGVmaW5pdGlvbnMgb2YgdGltaW5nIGFub21hbGllcywgYW5kIGlkZW50aWZ5IGV4YW1wbGVzIHdoZXJlIHRoZXkgZG8gbm90IGFsaWduIHdpdGggY29tbW9uIG9ic2VydmF0aW9ucy4gV2UgdGhlbiBwcm92aWRlIGEgZGVmaW5pdGlvbiBmb3IgY29uc2lzdGVudGx5IHNsb3dlciBoYXJkd2FyZSB0cmFjZXMgdGhhdCBjYW4gYmUgdXNlZCB0byBkZWZpbmUgdGltaW5nIGFub21hbGllcyBhbmQgYWxpZ25zIHdpdGggY29tbW9uIG9ic2VydmF0aW9ucy59LAogIGNhdGVnb3J5PSB7d2NldH0sCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWYsd2NldH0sCiAga2V5d29yZHMgPSB7d2NldH0sCiAgIHB1Ymxpc2hlciA9IHtTY2hsb3NzIERhZ3N0dWhsIC0gTGVpYm5pei1aZW50cnVtIGZ1ZXIgSW5mb3JtYXRpa30sCiAgc2VyaWVzICAgID0ge09BU0lDU30sCiAgdm9sdW1lICAgID0gezIzfSwKICAgICAgICBUeXBlID0ge0IgLSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2VzfSwKCn0KCgoKCkBpbnByb2NlZWRpbmdze2Nhc3Nlei1hY3NkLTIwMTEsCiAgYXV0aG9yICAgID0ge0ZyYW5jayBDYXNzZXp9LAogIHRpdGxlICAgICA9IHtUaW1lZCBHYW1lcyBmb3IgQ29tcHV0aW5nIHtXQ0VUfSBmb3IgUGlwZWxpbmVkIFByb2Nlc3NvcnMgd2l0aCBDYWNoZXN9LAogIGJvb2t0aXRsZSA9IHsxMXRoIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbiBBcHBsaWNhdGlvbiBvZiBDb25jdXJyZW5jeSB0byBTeXN0ZW0KICAgICAgICAgICAgICAgRGVzaWduLCB7QUNTRH0gMjAxMSwgTmV3Y2FzdGxlIFVwb24gVHluZSwgVUssIDIwLTI0IEp1bmUsIDIwMTF9LAogIHBhZ2VzICAgICA9IHsxOTUtLTIwNH0sCiAgeWVhciAgICAgID0gezIwMTF9LAogIHB1Ymxpc2hlciA9IHt7SUVFRX19LAogIHVybCAgICAgICA9IHtodHRwOi8vZG9pLmllZWVjb21wdXRlcnNvY2lldHkub3JnLzEwLjExMDkvQUNTRC4yMDExLjE1fSwKICBkb2kgICAgICAgPSB7MTAuMTEwOS9BQ1NELjIwMTEuMTV9LAogIHRpbWVzdGFtcCA9IHtXZWQsIDE1IEZlYiAyMDEyIDA5OjU5OjQzICswMTAwfSwKICBiaWJ1cmwgICAgPSB7aHR0cDovL2RibHAudW5pLXRyaWVyLmRlL3JlYy9iaWIvY29uZi9hY3NkL0Nhc3NlejExfSwKICBiaWJzb3VyY2UgPSB7ZGJscCBjb21wdXRlciBzY2llbmNlIGJpYmxpb2dyYXBoeSwgaHR0cDovL2RibHAub3JnfSwKICAgdXJscGFwZXIgPSB7cGFwZXJzL2Fjc2QtMjAxMS5wZGZ9LAogIHVybHNsaWRlcyA9IHtwYXBlcnMvc2xpZGVzLWFjc2QtMjAxMS5wZGZ9LAogIEFCU1RSQUNUID0ge0luIHRoaXMgcGFwZXIgd2UgaW50cm9kdWNlIGEgZnJhbWV3b3JrIGZvciBjb21wdXRpbmcgdXBwZXIgYm91bmRzIHlldAphY2N1cmF0ZSBXQ0VUIGZvciBoYXJkd2FyZSBwbGF0Zm9ybXMgd2l0aCBjYWNoZXMgYW5kIHBpcGVsaW5lcy4gVGhlIG1ldGhvZG9sb2d5CndlIHByb3Bvc2UgY29uc2lzdHMgb2YgMyBzdGVwczogMSkgZ2l2ZW4gYSBwcm9ncmFtIHRvIGFuYWx5c2UsIGNvbXB1dGUgYW4KZXF1aXZhbGVudCAoV0NFVC13aXNlKSBhYnN0cmFjdCBwcm9ncmFtOyAyKSBidWlsZCBhIHRpbWVkIGdhbWUgYnkgY29tcG9zaW5nCnRoaXMgYWJzdHJhY3QgcHJvZ3JhbSB3aXRoIGEgbmV0d29yayBvZiB0aW1lZCBhdXRvbWF0YSBtb2RlbGluZyB0aGUKYXJjaGl0ZWN0dXJlOyBhbmQgMykgY29tcHV0ZSB0aGUgV0NFVCBhcyB0aGUgb3B0aW1hbCB0aW1lIHRvIHJlYWNoIGEgd2lubmluZwpzdGF0ZSBpbiB0aGlzIGdhbWUuIFdlIGRlbW9uc3RyYXRlIHRoZSBhcHBsaWNhYmlsaXR5IG9mIG91ciBmcmFtZXdvcmsgb24Kc3RhbmRhcmQgYmVuY2htYXJrcyBmb3IgYW4gQVJNOSBwcm9jZXNzb3Igd2l0aCBpbnN0cnVjdGlvbiBhbmQgZGF0YSBjYWNoZXMsIGFuZApjb21wdXRlIHRoZSBXQ0VUIHdpdGggVVBQQUFMLVRpR0EuIFdlIGFsc28gc2hvdyB0aGF0IHRoaXMgZnJhbWV3b3JrIGNhbiBlYXNpbHkKYmUgZXh0ZW5kZWQgdG8gdGFrZSBpbnRvIGFjY291bnQgZHluYW1pYyBjaGFuZ2VzIGluIHRoZSBzcGVlZCBvZiB0aGUgcHJvY2Vzc29yCmR1cmluZyBwcm9ncmFtIGV4ZWN1dGlvbi4KfSwKZWUgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuMTEwOS9BQ1NELjIwMTEuMTV9LAogIGtleXdvcmRzID0ge3djZXQsIHRpbWVkIGF1dG9tYXRhfSwKICBjYXRlZ29yeSA9IHt3Y2V0fSwKICBzaG93ID0ge30sCiAgY2F0ZWdvcnk9IHt3Y2V0fSwKICBteXdlYnBhZ2UgPSB7d2NldH0sCiAgICAgICAgVHlwZSA9IHtCIC0gSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlc30sCgp9CgoKCgpAYXJ0aWNsZXtiZWNoLXdjZXQtMjAxMSwKICBhdXRob3IgICAgPSB7SmVhbnstfUx1YyBCe1wne2V9fWNoZW5uZWMgYW5kCiAgICAgICAgICAgICAgIEZyYW5jayBDYXNzZXp9LAogIHRpdGxlICAgICA9IHtDb21wdXRhdGlvbiBvZiB7V0NFVH0gdXNpbmcgUHJvZ3JhbSBTbGljaW5nIGFuZCBSZWFsLVRpbWUgTW9kZWwtQ2hlY2tpbmd9LAogIGpvdXJuYWwgICA9IHtDb1JSfSwKICBUeXBlID0ge0UgLSBSZXBvcnRzfSwKICB2b2x1bWUgICAgPSB7YWJzLzExMDUuMTYzM30sCiAgeWVhciAgICAgID0gezIwMTF9LAogIHVybHBhcGVyICAgICAgID0ge2h0dHA6Ly9hcnhpdi5vcmcvYWJzLzExMDUuMTYzM30sCiAgdGltZXN0YW1wID0ge01vbiwgMDUgRGVjIDIwMTEgMTg6MDU6MzIgKzAxMDB9LAogIGJpYnVybCAgICA9IHtodHRwOi8vZGJscC51bmktdHJpZXIuZGUvcmVjL2JpYi9qb3VybmFscy9jb3JyL2Ficy0xMTA1LTE2MzN9LAogIGJpYnNvdXJjZSA9IHtkYmxwIGNvbXB1dGVyIHNjaWVuY2UgYmlibGlvZ3JhcGh5LCBodHRwOi8vZGJscC5vcmd9LAogIEFCU1RSQUNUID0geyBDb21wdXRpbmcgYWNjdXJhdGUgV0NFVCBvbiBtb2Rlcm4gY29tcGxleCBhcmNoaXRlY3R1cmVzIGlzIGEgY2hhbGxlbmdpbmcgdGFzay4gVGhpcyBwcm9ibGVtIGhhcyBiZWVuIGRldm90ZWQgYSBsb3Qgb2YgYXR0ZW50aW9uIGluIHRoZSBsYXN0IGRlY2FkZSBidXQgdGhlcmUgYXJlIHN0aWxsIHNvbWUgb3BlbiBpc3N1ZXMuIEZpcnN0LCB0aGUgY29udHJvbCBmbG93IGdyYXBoIChDRkcpIG9mIGEgYmluYXJ5IHByb2dyYW0gaXMgbmVlZGVkIHRvIGNvbXB1dGUgdGhlIFdDRVQgYW5kIHRoaXMgQ0ZHIGlzIGJ1aWx0IHVzaW5nIHNvbWUgaW50ZXJuYWwga25vd2xlZGdlIG9mIHRoZSBjb21waWxlciB0aGF0IGdlbmVyYXRlZCB0aGUgYmluYXJ5IGNvZGU7IG1vcmVvdmVyIG9uY2UgY29uc3RydWN0ZWQgdGhlIENGRyBoYXMgdG8gYmUgbWFudWFsbHkgYW5ub3RhdGVkIHdpdGggbG9vcCBib3VuZHMuIFNlY29uZCwgdGhlIGFsZ29yaXRobXMgdG8gY29tcHV0ZSB0aGUgV0NFVCAoY29tYmluaW5nIEFic3RyYWN0IEludGVycHJldGF0aW9uIGFuZCBJbnRlZ2VyIExpbmVhciBQcm9ncmFtbWluZykgYXJlIHRhaWxvcmVkIGZvciBzcGVjaWZpYyBhcmNoaXRlY3R1cmVzOiBjaGFuZ2luZyB0aGUgYXJjaGl0ZWN0dXJlIChlLmcuIHJlcGxhY2luZyBhbiBBUk03IGJ5IGFuIEFSTTkpIHJlcXVpcmVzIHRoZSBkZXNpZ24gb2YgYSBuZXcgYWQgaG9jIGFsZ29yaXRobS4gVGhpcmQsIHRoZSB0aWdodG5lc3Mgb2YgdGhlIGNvbXB1dGVkIHJlc3VsdHMgKG9idGFpbmVkIHVzaW5nIHRoZSBhdmFpbGFibGUgdG9vbHMpIGFyZSBub3QgY29tcGFyZWQgdG8gYWN0dWFsIGV4ZWN1dGlvbiB0aW1lcyBtZWFzdXJlZCBvbiB0aGUgcmVhbCBoYXJkd2FyZS4gSW4gdGhpcyBwYXBlciB3ZSBhZGRyZXNzIHRoZSBhYm92ZSBtZW50aW9uZWQgcHJvYmxlbXMuIFdlIGZpcnN0IGRlc2NyaWJlIGEgZnVsbHkgYXV0b21hdGljIG1ldGhvZCB0byBjb21wdXRlIGEgQ0ZHIGJhc2VkIHNvbGVseSBvbiB0aGUgYmluYXJ5IHByb2dyYW0gdG8gYW5hbHlzZS4gU2Vjb25kLCB3ZSBkZXNjcmliZSB0aGUgbW9kZWwgb2YgdGhlIGhhcmR3YXJlIGFzIGEgcHJvZHVjdCBvZiB0aW1lZCBhdXRvbWF0YSwgYW5kIHRoaXMgbW9kZWwgaXMgaW5kZXBlbmRlbnQgZnJvbSB0aGUgcHJvZ3JhbSBkZXNjcmlwdGlvbi4gVGhlIG1vZGVsIG9mIGEgcHJvZ3JhbSBydW5uaW5nIG9uIGEgaGFyZHdhcmUgaXMgb2J0YWluZWQgYnkgc3luY2hyb25pemluZyAodGhlIGF1dG9tYXRvbiBvZikgdGhlIHByb2dyYW0gd2l0aCB0aGUgKHRpbWVkIGF1dG9tYXRhKSBtb2RlbCBvZiB0aGUgaGFyZHdhcmUuIENvbXB1dGluZyB0aGUgV0NFVCBpcyByZWR1Y2VkIHRvIGEgcmVhY2hhYmlsaXR5IHByb2JsZW0gb24gdGhlIHN5bmNocm9uaXNlZCBtb2RlbCBhbmQgc29sdmVkIHVzaW5nIHRoZSBtb2RlbC1jaGVja2VyIFVQUEFBTC4gRmluYWxseSwgd2UgcHJlc2VudCBhIHJpZ29yb3VzIG1ldGhvZG9sb2d5IHRoYXQgZW5hYmxlcyB1cyB0byBjb21wYXJlIG91ciBjb21wdXRlZCByZXN1bHRzIHRvIGFjdHVhbCBleGVjdXRpb24gdGltZXMgbWVhc3VyZWQgb24gYSByZWFsIHBsYXRmb3JtLCB0aGUgQVJNOTIwVC59LAogICAgY2F0ZWdvcnk9IHt3Y2V0fSwKICBrZXl3b3JkcyA9IHt3Y2V0LCB0aW1lZCBhdXRvbWF0YX0sCiAgc2hvdyA9IHt9LAogIG15d2VicGFnZSA9IHt3Y2V0fQp9CgoKCkBhcnRpY2xle0RCTFA6am91cm5hbHMvY29yci9hYnMtMTAwNi0xOTUxLAogIGF1dGhvciAgICA9IHtGcmFuY2sgQ2Fzc2V6fSwKICB0aXRsZSAgICAgPSB7VGltZWQgR2FtZXMgZm9yIENvbXB1dGluZyBXb3JzdC1DYXNlIEV4ZWN1dGlvbi1UaW1lc30sCiAgam91cm5hbCAgID0ge0NvUlJ9LAogIFR5cGUgPSB7RSAtIFJlcG9ydHN9LAogIHZvbHVtZSAgICA9IHthYnMvMTAwNi4xOTUxfSwKICB5ZWFyICAgICAgPSB7MjAxMH0sCiAgdXJsICAgICAgID0ge2h0dHA6Ly9hcnhpdi5vcmcvYWJzLzEwMDYuMTk1MX0sCiAgdGltZXN0YW1wID0ge01vbiwgMDUgRGVjIDIwMTEgMTg6MDQ6NTQgKzAxMDB9LAogIGJpYnVybCAgICA9IHtodHRwOi8vZGJscC51bmktdHJpZXIuZGUvcmVjL2JpYi9qb3VybmFscy9jb3JyL2Ficy0xMDA2LTE5NTF9LAogIGJpYnNvdXJjZSA9IHtkYmxwIGNvbXB1dGVyIHNjaWVuY2UgYmlibGlvZ3JhcGh5LCBodHRwOi8vZGJscC5vcmd9LAogICAga2V5d29yZHMgPSB7d2NldCwgdGltZWQgYXV0b21hdGF9LAoKICBhYnN0cmFjdD0ge0luIHRoaXMgcGFwZXIgd2UgaW50cm9kdWNlIGEgZnJhbWV3b3JrIGZvciBjb21wdXRpbmcgdXBwZXIgYm91bmRzIHlldCBhY2N1cmF0ZSBXQ0VUIGZvciBoYXJkd2FyZSBwbGF0Zm9ybXMgd2l0aCBjYWNoZXMgYW5kIHBpcGVsaW5lcy4gVGhlIG1ldGhvZG9sb2d5IHdlIHByb3Bvc2UgY29uc2lzdHMgb2YgMyBzdGVwczogMSkgZ2l2ZW4gYSBwcm9ncmFtIHRvIGFuYWx5c2UsIGNvbXB1dGUgYW4gZXF1aXZhbGVudCAoV0NFVC13aXNlKSBhYnN0cmFjdCBwcm9ncmFtOyAyKSBidWlsZCBhIHRpbWVkIGdhbWUgYnkgY29tcG9zaW5nIHRoaXMgYWJzdHJhY3QgcHJvZ3JhbSB3aXRoIGEgbmV0d29yayBvZiB0aW1lZCBhdXRvbWF0YSBtb2RlbGluZyB0aGUgYXJjaGl0ZWN0dXJlOyBhbmQgMykgY29tcHV0ZSB0aGUgV0NFVCBhcyB0aGUgb3B0aW1hbCB0aW1lIHRvIHJlYWNoIGEgd2lubmluZyBzdGF0ZSBpbiB0aGlzIGdhbWUuIFdlIGRlbW9uc3RyYXRlIHRoZSBhcHBsaWNhYmlsaXR5IG9mIG91ciBmcmFtZXdvcmsgb24gc3RhbmRhcmQgYmVuY2htYXJrcyBmb3IgYW4gQVJNOSBwcm9jZXNzb3Igd2l0aCBpbnN0cnVjdGlvbiBhbmQgZGF0YSBjYWNoZXMsIGFuZCBjb21wdXRlIHRoZSBXQ0VUIHdpdGggVVBQQUFMLVRpR0EuIFdlIGFsc28gc2hvdyB0aGF0IHRoaXMgZnJhbWV3b3JrIGNhbiBlYXNpbHkgYmUgZXh0ZW5kZWQgdG8gdGFrZSBpbnRvIGFjY291bnQgZHluYW1pYyBjaGFuZ2VzIGluIHRoZSBzcGVlZCBvZiB0aGUgcHJvY2Vzc29yIGR1cmluZyBwcm9ncmFtIGV4ZWN1dGlvbi59Cn0KCgolJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQolJSUgMjAwOQolJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQoK\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=keywords:wcet&amp;css=true&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=keywords:wcet&amp;css=true\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=keywords:wcet&amp;css=true\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\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      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. 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    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2016\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2016')\"\n      onkeypress=\"toggleGroup('group_2016')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2016</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/ieee-systems-2016.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016', 'http://science.mq.edu.au/~fcassez/bib/papers/ieee-systems-2016.pdf', event);\">\n    Efficient and Scalable Runtime Monitoring for Cyber–Physical System.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Zheng, X.; Julien, C.; Podorozhny, R.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Rakotoarivelo, T.\n</span>\n\n  \n\n</span>\n\n  <i>IEEE Systems Journal</i>, 99: 1–12. October 2016.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/ieee-systems-2016.pdf\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016', 'http://science.mq.edu.au/~fcassez/bib/papers/ieee-systems-2016.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Efficient and Scalable Runtime Monitoring for Cyber–Physical System [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://ieeexplore.ieee.org/document/7605519/\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016', 'http://ieeexplore.ieee.org/document/7605519/', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Efficient and Scalable Runtime Monitoring for Cyber–Physical System [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1109/JSYST.2016.2614599\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016', 'http://doi.org/10.1109/JSYST.2016.2614599', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('zheng-julien-podorozhny-cassez-rakotoarivelo-efficientandscalableruntimemonitoringforcyberphysicalsystem-2016')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2015\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2015')\"\n      onkeypress=\"toggleGroup('group_2015')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2015</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/mass-2015.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/mass-2015.pdf', event);\">\n    BraceAssertion: Runtime Verification of Cyber-Physical Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Zheng, X.; Julien, C.; Podorozhny, R.;  and <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>\n</span>\n\n  \n\n</span>\n\n  In <i>12th IEEE International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015, Dallas, TX, USA, October 19-22, 2015</i>, pages 298–306,  2015. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/mass-2015.pdf\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/mass-2015.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"BraceAssertion: Runtime Verification of Cyber-Physical Systems [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1109/MASS.2015.15\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015', 'http://dx.doi.org/10.1109/MASS.2015.15', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"BraceAssertion: Runtime Verification of Cyber-Physical Systems [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1109/MASS.2015.15\"\n     onclick=\"log_download('zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015', 'http://doi.org/10.1109/MASS.2015.15', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/slides-mars-2015.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/slides-mars-2015.pdf', event);\">\n    Timed Automata for Modelling Caches and Pipelines.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and de Aledo Marugán, P. G.\n</span>\n\n  \n\n</span>\n\n  In van Glabbeek, R. J.; Groote, J. F.;  and Höfner, P., editor(s), <i>Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, November 23, 2015.</i>, volume 196, of <i>EPTCS</i>, pages 37–45,  2015. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dx.doi.org/10.4204/EPTCS.196.4\"\n     onclick=\"log_download('cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015', 'http://dx.doi.org/10.4204/EPTCS.196.4', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Timed Automata for Modelling Caches and Pipelines [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/slides-mars-2015.pdf\"\n     onclick=\"log_download('cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/slides-mars-2015.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timed Automata for Modelling Caches and Pipelines [pdf]\"\n       title=\"Slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Slides</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.4204/EPTCS.196.4\"\n     onclick=\"log_download('cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015', 'http://doi.org/10.4204/EPTCS.196.4', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-dealedomarugn-timedautomataformodellingcachesandpipelines-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{cassez-mars-2015,\n  author    = {Franck Cassez and\n               Pablo Gonz{\\&#x27;{a}}lez de Aledo Marug{\\&#x27;{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{\\&quot;{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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2013\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2013')\"\n      onkeypress=\"toggleGroup('group_2013')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2013</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2013.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/acsd-2013.pdf', event);\">\n    Timing Analysis of Binary Programs with UPPAAL.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Béchennec, J.\n</span>\n\n  \n\n</span>\n\n  In <i>13th International Conference on Application of Concurrency to System Design, ACSD 2013</i>, pages 41-50, July 2013. IEEE Computer Society\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2013.pdf\"\n     onclick=\"log_download('cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/acsd-2013.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timing Analysis of Binary Programs with UPPAAL [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-wcet-2013.pdf\"\n     onclick=\"log_download('cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-wcet-2013.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timing Analysis of Binary Programs with UPPAAL [pdf]\"\n       title=\"Slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Slides</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/http://dx.doi.org/10.1109/ACSD.2013.7\"\n     onclick=\"log_download('cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013', 'http://doi.org/http://dx.doi.org/10.1109/ACSD.2013.7', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>3 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-bchennec-timinganalysisofbinaryprogramswithuppaal-2013')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2012\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2012')\"\n      onkeypress=\"toggleGroup('group_2012')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2012</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-hansen-olesen-whatisatiminganomaly-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf', event);\">\n    What is a Timing Anomaly?.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Hansen, R. R.;  and Olesen, M. C.\n</span>\n\n  \n\n</span>\n\n  In <i>12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy</i>, volume 23, of <i>OASICS</i>, pages 1-12,  2012. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\"\n     onclick=\"log_download('cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"What is a Timing Anomaly? [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\"\n     onclick=\"log_download('cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://dx.doi.org/10.4230/OASIcs.WCET.2012.1', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"What is a Timing Anomaly? [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-hansen-olesen-whatisatiminganomaly-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-hansen-olesen-whatisatiminganomaly-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2011\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2011')\"\n      onkeypress=\"toggleGroup('group_2011')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2011</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011', 'http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf', event);\">\n    Timed Games for Computing WCET for Pipelined Processors with Caches.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>\n</span>\n\n  \n\n</span>\n\n  In <i>11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011</i>, pages 195–204,  2011. IEEE\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf\"\n     onclick=\"log_download('cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011', 'http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timed Games for Computing WCET for Pipelined Processors with Caches [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-2011.pdf\"\n     onclick=\"log_download('cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011', 'http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-2011.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timed Games for Computing WCET for Pipelined Processors with Caches [pdf]\"\n       title=\"Slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Slides</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1109/ACSD.2011.15\"\n     onclick=\"log_download('cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011', 'http://dx.doi.org/10.1109/ACSD.2011.15', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Timed Games for Computing WCET for Pipelined Processors with Caches [link]\"\n       title=\"Link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1109/ACSD.2011.15\"\n     onclick=\"log_download('cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011', 'http://doi.org/10.1109/ACSD.2011.15', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://arxiv.org/abs/1105.1633\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011', 'http://arxiv.org/abs/1105.1633', event);\">\n    Computation of WCET using Program Slicing and Real-Time Model-Checking.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Béchennec, J.;  and <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>\n</span>\n\n  \n\n</span>\n\n  <i>CoRR</i>, abs/1105.1633.  2011.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://arxiv.org/abs/1105.1633\"\n     onclick=\"log_download('bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011', 'http://arxiv.org/abs/1105.1633', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Computation of WCET using Program Slicing and Real-Time Model-Checking [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bchennec-cassez-computationofwcetusingprogramslicingandrealtimemodelchecking-2011')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{bech-wcet-2011,\n  author    = {Jean{-}Luc B{\\&#x27;{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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2010\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2010')\"\n      onkeypress=\"toggleGroup('group_2010')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2010</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-timedgamesforcomputingworstcaseexecutiontimes-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://arxiv.org/abs/1006.1951\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-timedgamesforcomputingworstcaseexecutiontimes-2010', 'http://arxiv.org/abs/1006.1951', event);\">\n    Timed Games for Computing Worst-Case Execution-Times.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>\n</span>\n\n  \n\n</span>\n\n  <i>CoRR</i>, abs/1006.1951.  2010.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://arxiv.org/abs/1006.1951\"\n     onclick=\"log_download('cassez-timedgamesforcomputingworstcaseexecutiontimes-2010', 'http://arxiv.org/abs/1006.1951', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Timed Games for Computing Worst-Case Execution-Times [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-timedgamesforcomputingworstcaseexecutiontimes-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-timedgamesforcomputingworstcaseexecutiontimes-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);