---
_id: '6035'
abstract:
- lang: eng
  text: 'We present JuliaReach, a toolbox for set-based reachability analysis of dynamical
    systems. JuliaReach consists of two main packages: Reachability, containing implementations
    of reachability algorithms for continuous and hybrid systems, and LazySets, a
    standalone library that implements state-of-the-art algorithms for calculus with
    convex sets. The library offers both concrete and lazy set representations, where
    the latter stands for the ability to delay set computations until they are needed.
    The choice of the programming language Julia and the accompanying documentation
    of our toolbox allow researchers to easily translate set-based algorithms from
    mathematics to software in a platform-independent way, while achieving runtime
    performance that is comparable to statically compiled languages. Combining lazy
    operations in high dimensions and explicit computations in low dimensions, JuliaReach
    can be applied to solve complex, large-scale problems.'
article_processing_charge: No
arxiv: 1
author:
- first_name: Sergiy
  full_name: Bogomolov, Sergiy
  id: 369D9A44-F248-11E8-B48F-1D18A9856A87
  last_name: Bogomolov
  orcid: 0000-0002-0686-0365
- first_name: Marcelo
  full_name: Forets, Marcelo
  last_name: Forets
- first_name: Goran
  full_name: Frehse, Goran
  last_name: Frehse
- first_name: Kostiantyn
  full_name: Potomkin, Kostiantyn
  last_name: Potomkin
- first_name: Christian
  full_name: Schilling, Christian
  id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
  last_name: Schilling
  orcid: 0000-0003-3658-1065
citation:
  ama: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox
    for set-based reachability. In: <i>Proceedings of the 22nd International Conference
    on Hybrid Systems: Computation and Control</i>. Vol 22. ACM; 2019:39-44. doi:<a
    href="https://doi.org/10.1145/3302504.3311804">10.1145/3302504.3311804</a>'
  apa: 'Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., &#38; Schilling, C. (2019).
    JuliaReach: A toolbox for set-based reachability. In <i>Proceedings of the 22nd
    International Conference on Hybrid Systems: Computation and Control</i> (Vol.
    22, pp. 39–44). Montreal, QC, Canada: ACM. <a href="https://doi.org/10.1145/3302504.3311804">https://doi.org/10.1145/3302504.3311804</a>'
  chicago: 'Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin,
    and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In
    <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation
    and Control</i>, 22:39–44. ACM, 2019. <a href="https://doi.org/10.1145/3302504.3311804">https://doi.org/10.1145/3302504.3311804</a>.'
  ieee: 'S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach:
    A toolbox for set-based reachability,” in <i>Proceedings of the 22nd International
    Conference on Hybrid Systems: Computation and Control</i>, Montreal, QC, Canada,
    2019, vol. 22, pp. 39–44.'
  ista: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach:
    A toolbox for set-based reachability. Proceedings of the 22nd International Conference
    on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and
    Control vol. 22, 39–44.'
  mla: 'Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.”
    <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation
    and Control</i>, vol. 22, ACM, 2019, pp. 39–44, doi:<a href="https://doi.org/10.1145/3302504.3311804">10.1145/3302504.3311804</a>.'
  short: 'S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings
    of the 22nd International Conference on Hybrid Systems: Computation and Control,
    ACM, 2019, pp. 39–44.'
conference:
  end_date: 2019-04-18
  location: Montreal, QC, Canada
  name: 'HSCC: Hybrid Systems Computation and Control'
  start_date: 2019-04-16
date_created: 2019-02-18T14:43:28Z
date_published: 2019-04-16T00:00:00Z
date_updated: 2023-08-24T14:47:21Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3302504.3311804
ec_funded: 1
external_id:
  arxiv:
  - '1901.10736'
  isi:
  - '000516713900005'
file:
- access_level: open_access
  checksum: 28ed56439aea5991c3122d4730fd828f
  content_type: application/pdf
  creator: cschilli
  date_created: 2019-03-05T09:27:18Z
  date_updated: 2020-07-14T12:47:17Z
  file_id: '6067'
  file_name: hscc19.pdf
  file_size: 3784414
  relation: main_file
file_date_updated: 2020-07-14T12:47:17Z
has_accepted_license: '1'
intvolume: '        22'
isi: 1
keyword:
- reachability analysis
- hybrid systems
- lazy computation
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 39-44
project:
- _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
- _id: 260C2330-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '754411'
  name: ISTplus - Postdoctoral Fellowships
publication: 'Proceedings of the 22nd International Conference on Hybrid Systems:
  Computation and Control'
publication_identifier:
  isbn:
  - '9781450362825'
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'JuliaReach: A toolbox for set-based reachability'
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 22
year: '2019'
...
---
_id: '6428'
abstract:
- lang: eng
  text: 'Safety and security are major concerns in the development of Cyber-Physical
    Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify
    and monitor the correctness of CPS relativeto formalized requirements. Incorporating
    STL into a developmentprocess enables designers to automatically monitor and diagnosetraces,
    compute robustness estimates based on requirements, andperform requirement falsification,
    leading to productivity gains inverification and validation activities; however,
    in its current formSTL is agnostic to the input/output classification of signals,
    andthis negatively impacts the relevance of the analysis results.In this paper
    we propose to make the interface explicit in theSTL language by introducing input/output
    signal declarations. Wethen define new measures of input vacuity and output robustnessthat
    better reflect the nature of the system and the specification in-tent. The resulting
    framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification
    and validation activities.We demonstrate the benefits of IA-STL on several CPS
    analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand
    (3) fault localization. We describe an implementation of our en-hancement to STL
    and associated notions of robustness and vacuityin a prototype extension of Breach,
    a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these
    methodologi-cal improvements and evaluate our results on two examples fromthe
    automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell
    system.'
article_processing_charge: No
author:
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- first_name: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
- first_name: Alexandre
  full_name: Donzé, Alexandre
  last_name: Donzé
- first_name: Hisahiro
  full_name: Ito, Hisahiro
  last_name: Ito
- first_name: James
  full_name: Kapinski, James
  last_name: Kapinski
citation:
  ama: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal
    temporal logic. In: <i>Proceedings of the 2019 22nd ACM International Conference
    on Hybrid Systems: Computation and Control</i>. ACM; 2019:57-66. doi:<a href="https://doi.org/10.1145/3302504.3311800">10.1145/3302504.3311800</a>'
  apa: 'Ferrere, T., Nickovic, D., Donzé, A., Ito, H., &#38; Kapinski, J. (2019).
    Interface-aware signal temporal logic. In <i>Proceedings of the 2019 22nd ACM
    International Conference on Hybrid Systems: Computation and Control</i> (pp. 57–66).
    Montreal, Canada: ACM. <a href="https://doi.org/10.1145/3302504.3311800">https://doi.org/10.1145/3302504.3311800</a>'
  chicago: 'Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James
    Kapinski. “Interface-Aware Signal Temporal Logic.” In <i>Proceedings of the 2019
    22nd ACM International Conference on Hybrid Systems: Computation and Control</i>,
    57–66. ACM, 2019. <a href="https://doi.org/10.1145/3302504.3311800">https://doi.org/10.1145/3302504.3311800</a>.'
  ieee: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware
    signal temporal logic,” in <i>Proceedings of the 2019 22nd ACM International Conference
    on Hybrid Systems: Computation and Control</i>, Montreal, Canada, 2019, pp. 57–66.'
  ista: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware
    signal temporal logic. Proceedings of the 2019 22nd ACM International Conference
    on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and
    Control, 57–66.'
  mla: 'Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” <i>Proceedings
    of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and
    Control</i>, ACM, 2019, pp. 57–66, doi:<a href="https://doi.org/10.1145/3302504.3311800">10.1145/3302504.3311800</a>.'
  short: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings
    of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and
    Control, ACM, 2019, pp. 57–66.'
conference:
  end_date: 2019-04-18
  location: Montreal, Canada
  name: 'HSCC: Hybrid Systems Computation and Control'
  start_date: 2019-04-16
date_created: 2019-05-13T08:13:46Z
date_published: 2019-04-16T00:00:00Z
date_updated: 2023-08-25T10:19:23Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3302504.3311800
external_id:
  isi:
  - '000516713900007'
file:
- access_level: open_access
  checksum: b8e967081e051d1c55ca5d18fb187890
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-08T17:25:45Z
  date_updated: 2020-10-08T17:25:45Z
  file_id: '8633'
  file_name: 2019_ACM_Ferrere.pdf
  file_size: 1055421
  relation: main_file
  success: 1
file_date_updated: 2020-10-08T17:25:45Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 57-66
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 'Proceedings of the 2019 22nd ACM International Conference on Hybrid
  Systems: Computation and Control'
publication_identifier:
  isbn:
  - '9781450362825'
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface-aware signal temporal logic
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2019'
...