@inproceedings{mass-Zheng-15,
  author    = {Xi Zheng and
               Christine Julien and
               {Rodion M.} Podorozhny and
               Franck Cassez},
  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.},
  Type = {B - International Conferences},

}

{"_id":"2nuZCPZECSvoEwZ7M","bibbaseid":"zheng-julien-podorozhny-cassez-braceassertionruntimeverificationofcyberphysicalsystems-2015","author_short":["Zheng, X.","Julien, C.","Podorozhny, R.","Cassez, F."],"bibdata":{"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":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["qbqYFWskmoonRB43F","8742EsvjQfyP2fYBW"],"keywords":["wcet","timed automata"],"search_terms":["braceassertion","runtime","verification","cyber","physical","systems","zheng","julien","podorozhny","cassez"],"title":"BraceAssertion: Runtime Verification of Cyber-Physical Systems","year":2015}