---
_id: '1606'
abstract:
- lang: eng
  text: 'In this paper, we present the first steps toward a runtime verification framework
    for monitoring hybrid and cyber-physical systems (CPS) development tools based
    on randomized differential testing. The development tools include hybrid systems
    reachability analysis tools, model-based development environments like Simulink/Stateflow
    (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these
    hybrid automaton models are translated to a number of different tools (currently,
    SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using
    the HyST source transformation and translation tool. Then, the hybrid automaton
    models are executed in the different tools and their outputs are parsed. The final
    step is the differential comparison: the outputs of the different tools are compared.
    If the results do not agree (in the sense that an analysis or verification result
    from one tool does not match that of another tool, ignoring timeouts, etc.), a
    candidate bug is flagged and the model is saved for future analysis by the user.
    The process then repeats and the monitoring continues until the user terminates
    the process. We present preliminary results that have been useful in identifying
    a few bugs in the analysis methods of different development tools, and in an earlier
    version of HyST.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luan
  full_name: Nguyen, Luan
  last_name: Nguyen
- first_name: Christian
  full_name: Schilling, Christian
  last_name: Schilling
- first_name: Sergiy
  full_name: Bogomolov, Sergiy
  id: 369D9A44-F248-11E8-B48F-1D18A9856A87
  last_name: Bogomolov
  orcid: 0000-0002-0686-0365
- first_name: Taylor
  full_name: Johnson, Taylor
  last_name: Johnson
citation:
  ama: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid
    analysis tools. In: <i>6th International Conference</i>. Vol 9333. Springer Nature;
    2015:281-286. doi:<a href="https://doi.org/10.1007/978-3-319-23820-3_19">10.1007/978-3-319-23820-3_19</a>'
  apa: 'Nguyen, L., Schilling, C., Bogomolov, S., &#38; Johnson, T. (2015). Runtime
    verification for hybrid analysis tools. In <i>6th International Conference</i>
    (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. <a href="https://doi.org/10.1007/978-3-319-23820-3_19">https://doi.org/10.1007/978-3-319-23820-3_19</a>'
  chicago: Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson.
    “Runtime Verification for Hybrid Analysis Tools.” In <i>6th International Conference</i>,
    9333:281–86. Springer Nature, 2015. <a href="https://doi.org/10.1007/978-3-319-23820-3_19">https://doi.org/10.1007/978-3-319-23820-3_19</a>.
  ieee: L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification
    for hybrid analysis tools,” in <i>6th International Conference</i>, Vienna, Austria,
    2015, vol. 9333, pp. 281–286.
  ista: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification
    for hybrid analysis tools. 6th International Conference. RV: Runtime Verification,
    LNCS, vol. 9333, 281–286.'
  mla: Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” <i>6th
    International Conference</i>, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:<a
    href="https://doi.org/10.1007/978-3-319-23820-3_19">10.1007/978-3-319-23820-3_19</a>.
  short: L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International
    Conference, Springer Nature, 2015, pp. 281–286.
conference:
  end_date: 2015-09-25
  location: Vienna, Austria
  name: 'RV: Runtime Verification'
  start_date: 2015-09-22
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-15T00:00:00Z
date_updated: 2022-02-01T14:52:59Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-319-23820-3_19
ec_funded: 1
intvolume: '      9333'
language:
- iso: eng
month: '11'
oa_version: None
page: 281 - 286
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: 6th International Conference
publication_identifier:
  isbn:
  - 978-3-319-23819-7
publication_status: published
publisher: Springer Nature
publist_id: '5562'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Runtime verification for hybrid analysis tools
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9333
year: '2015'
...