---
_id: '14405'
abstract:
- lang: eng
text: We introduce hypernode automata as a new specification formalism for hyperproperties
of concurrent systems. They are finite automata with nodes labeled with hypernode
logic formulas and transitions labeled with actions. A hypernode logic formula
specifies relations between sequences of variable values in different system executions.
Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces
by constraining the values and the order of value changes of each variable without
correlating the timing of the changes. Different execution traces are synchronized
solely through the transitions of hypernode automata. Hypernode automata naturally
combine asynchronicity at the node level with synchronicity at the transition
level. We show that the model-checking problem for hypernode automata is decidable
over action-labeled Kripke structures, whose actions induce transitions of the
specification automata. For this reason, hypernode automaton is a suitable formalism
for specifying and verifying asynchronous hyperproperties, such as declassifying
observational determinism in multi-threaded programs.
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)
SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the
ERC Advanced Grant\r\nVAMOS 101020093."
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata.
In: 34th International Conference on Concurrency Theory. Vol 279. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2023). Hypernode automata. In 34th International Conference on Concurrency
Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21'
chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Hypernode Automata.” In 34th International Conference on Concurrency
Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
https://doi.org/10.4230/LIPIcs.CONCUR.2023.21.
ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode
automata,” in 34th International Conference on Concurrency Theory, Antwerp,
Belgium, 2023, vol. 279.
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode
automata. 34th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 279, 21.'
mla: Bartocci, Ezio, et al. “Hypernode Automata.” 34th International Conference
on Concurrency Theory, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.21.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th
International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023.
conference:
end_date: 2023-09-22
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-19
date_created: 2023-10-08T22:01:16Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:43:44Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.21
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 215765e40454d806174ac0a223e8d6fa
content_type: application/pdf
creator: dernst
date_created: 2023-10-09T07:42:45Z
date_updated: 2023-10-09T07:42:45Z
file_id: '14413'
file_name: 2023_LIPcs_Bartocci.pdf
file_size: 795790
relation: main_file
success: 1
file_date_updated: 2023-10-09T07:42:45Z
has_accepted_license: '1'
intvolume: ' 279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772990'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hypernode automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 279
year: '2023'
...
---
_id: '10774'
abstract:
- lang: eng
text: We study the problem of specifying sequential information-flow properties
of systems. Information-flow properties are hyperproperties, as they compare different
traces of a system. Sequential information-flow properties can express changes,
over time, in the information-flow constraints. For example, information-flow
constraints during an initialization phase of a system may be different from information-flow
constraints that are required during the operation phase. We formalize several
variants of interpreting sequential information-flow constraints, which arise
from different assumptions about what can be observed of the system. For this
purpose, we introduce a first-order logic, called Hypertrace Logic, with both
trace and time quantifiers for specifying linear-time hyperproperties. We prove
that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied variants of sequential
information flow, including all variants in which the transition between sequential
phases (such as initialization and operation) happens asynchronously. Our results
rely on new equivalences between sets of traces that cannot be distinguished by
certain classes of formulas from Hypertrace Logic. This presents a new approach
to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
information flow. In: Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Flavors of sequential information flow,” in Lecture Notes in Computer Science
(including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp.
1–19.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
of sequential information flow. Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
1–19.'
mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp.
1–19, doi:10.1007/978-3-030-94583-1_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
1–19.
conference:
end_date: 2022-01-18
location: Philadelphia, PA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2022-08-05T09:02:56Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
arxiv:
- '2105.02013'
intvolume: ' 13182'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030945824'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13182
year: '2022'
...
---
_id: '11355'
abstract:
- lang: eng
text: "Contract-based design is a promising methodology for taming the complexity
of developing sophisticated systems. A formal contract distinguishes between assumptions,
which are constraints that the designer of a component puts on the environments
in which the component can be used safely, and guarantees, which are promises
that the designer asks from the team that implements the component. A theory of
formal contracts can be formalized as an interface theory, which supports the
composition and refinement of both assumptions and guarantees.\r\nAlthough there
is a rich landscape of contract-based design methods that address functional and
extra-functional properties, we present the first interface theory that is designed
for ensuring system-wide security properties. Our framework provides a refinement
relation and a composition operation that support both incremental design and
independent implementability. We develop our theory for both stateless and stateful
interfaces. We illustrate the applicability of our framework with an example inspired
from the automotive domain."
acknowledgement: This project has received funding from the European Union’s Horizon
2020 research and innovation programme under grant agreement No 956123 and was funded
in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow
interfaces. In: Fundamental Approaches to Software Engineering. Vol 13241.
Springer Nature; 2022:3-22. doi:10.1007/978-3-030-99429-7_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Information-flow interfaces. In Fundamental Approaches to Software
Engineering (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99429-7_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Information-Flow Interfaces.” In Fundamental Approaches
to Software Engineering, 13241:3–22. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99429-7_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Information-flow interfaces,” in Fundamental Approaches to Software Engineering,
Munich, Germany, 2022, vol. 13241, pp. 3–22.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow
interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental
Approaches to Software Engineering, LNCS, vol. 13241, 3–22.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Fundamental Approaches
to Software Engineering, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:10.1007/978-3-030-99429-7_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.
conference:
end_date: 2022-04-07
location: Munich, Germany
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2022-04-02
date_created: 2022-05-08T22:01:44Z
date_published: 2022-03-29T00:00:00Z
date_updated: 2023-08-03T07:03:40Z
day: '29'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-99429-7_1
ec_funded: 1
external_id:
isi:
- '000782393600001'
file:
- access_level: open_access
checksum: 7f6f860b20b8de2a249e9c1b4eee15cf
content_type: application/pdf
creator: dernst
date_created: 2022-05-09T06:52:44Z
date_updated: 2022-05-09T06:52:44Z
file_id: '11357'
file_name: 2022_LNCS_Bartocci.pdf
file_size: 479146
relation: main_file
success: 1
file_date_updated: 2022-05-09T06:52:44Z
has_accepted_license: '1'
intvolume: ' 13241'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 3-22
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030994280'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-flow interfaces
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13241
year: '2022'
...
---
_id: '10861'
abstract:
- lang: eng
text: We introduce in this paper AMT2.0, a tool for qualitative and quantitative
analysis of hybrid continuous and Boolean signals that combine numerical values
and discrete events. The evaluation of the signals is based on rich temporal specifications
expressed in extended signal temporal logic, which integrates timed regular expressions
within signal temporal logic. The tool features qualitative monitoring (property
satisfaction checking), trace diagnostics for explaining and justifying property
violations and specification-driven measurement of quantitative features of the
signal. We demonstrate the tool functionality on several running examples and
case studies, and evaluate its performance.
article_processing_charge: No
article_type: original
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Olivier
full_name: Lebeltel, Olivier
last_name: Lebeltel
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Dogan
full_name: Ulus, Dogan
last_name: Ulus
citation:
ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and
quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 2020;22(6):741-758. doi:10.1007/s10009-020-00582-z'
apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2020).
AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal
logic. International Journal on Software Tools for Technology Transfer.
Springer Nature. https://doi.org/10.1007/s10009-020-00582-z'
chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan
Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal
Temporal Logic.” International Journal on Software Tools for Technology Transfer.
Springer Nature, 2020. https://doi.org/10.1007/s10009-020-00582-z.'
ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic,” International
Journal on Software Tools for Technology Transfer, vol. 22, no. 6. Springer
Nature, pp. 741–758, 2020.'
ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 22(6), 741–758.'
mla: 'Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis
with Extended Signal Temporal Logic.” International Journal on Software Tools
for Technology Transfer, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58,
doi:10.1007/s10009-020-00582-z.'
short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal
on Software Tools for Technology Transfer 22 (2020) 741–758.
date_created: 2022-03-18T10:10:53Z
date_published: 2020-08-03T00:00:00Z
date_updated: 2023-09-08T11:52:02Z
day: '03'
department:
- _id: ToHe
doi: 10.1007/s10009-020-00582-z
external_id:
isi:
- '000555398600001'
intvolume: ' 22'
isi: 1
issue: '6'
keyword:
- Information Systems
- Software
language:
- iso: eng
month: '08'
oa_version: None
page: 741-758
publication: International Journal on Software Tools for Technology Transfer
publication_identifier:
eissn:
- 1433-2787
issn:
- 1433-2779
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '299'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal
temporal logic'
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 22
year: '2020'
...
---
_id: '7232'
abstract:
- lang: eng
text: 'We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism
which extends STL by capturing the discrete/ continuous time duality found in
many cyber-physical systems (CPS), as well as mixed-signal electronic designs.
In STL−MX, properties of components with continuous dynamics are expressed in
STL, while specifications of components with discrete dynamics are written in
LTL. To combine the two layers, we evaluate formulas on two traces, discrete-
and continuous-time, and introduce two interface operators that map signals, properties
and their satisfaction signals across the two time domains. We show that STL-mx
has the expressive power of STL supplemented with an implicit T-periodic clock
signal. We develop and implement an algorithm for monitoring STL-mx formulas and
illustrate the approach using a mixed-signal example. '
alternative_title:
- LNCS
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: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: 17th
International Conference on Formal Modeling and Analysis of Timed Systems.
Vol 11750. Springer Nature; 2019:59-75. doi:10.1007/978-3-030-29662-9_4'
apa: 'Ferrere, T., Maler, O., & Nickovic, D. (2019). Mixed-time signal temporal
logic. In 17th International Conference on Formal Modeling and Analysis of
Timed Systems (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer
Nature. https://doi.org/10.1007/978-3-030-29662-9_4'
chicago: Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal
Logic.” In 17th International Conference on Formal Modeling and Analysis of
Timed Systems, 11750:59–75. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_4.
ieee: T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,”
in 17th International Conference on Formal Modeling and Analysis of Timed Systems,
Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.
ista: 'Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th
International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS:
Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.'
mla: Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” 17th International
Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer
Nature, 2019, pp. 59–75, doi:10.1007/978-3-030-29662-9_4.
short: T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on
Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Anaysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:48Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2023-09-06T14:57:17Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_4
external_id:
isi:
- '000611677700004'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 59-75
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: 17th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9661-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Mixed-time signal temporal logic
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
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: Proceedings of the 2019 22nd ACM International Conference
on Hybrid Systems: Computation and Control. ACM; 2019:57-66. doi:10.1145/3302504.3311800'
apa: 'Ferrere, T., Nickovic, D., Donzé, A., Ito, H., & Kapinski, J. (2019).
Interface-aware signal temporal logic. In Proceedings of the 2019 22nd ACM
International Conference on Hybrid Systems: Computation and Control (pp. 57–66).
Montreal, Canada: ACM. https://doi.org/10.1145/3302504.3311800'
chicago: 'Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James
Kapinski. “Interface-Aware Signal Temporal Logic.” In Proceedings of the 2019
22nd ACM International Conference on Hybrid Systems: Computation and Control,
57–66. ACM, 2019. https://doi.org/10.1145/3302504.3311800.'
ieee: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware
signal temporal logic,” in Proceedings of the 2019 22nd ACM International Conference
on Hybrid Systems: Computation and Control, 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.” Proceedings
of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and
Control, ACM, 2019, pp. 57–66, doi:10.1145/3302504.3311800.'
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'
...
---
_id: '299'
abstract:
- lang: eng
text: We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative
analysis of hybrid continuous and Boolean signals that combine numerical values
and discrete events. The evaluation of the signals is based on rich temporal specifications
expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular
Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative
monitoring (property satisfaction checking), trace diagnostics for explaining
and justifying property violations and specification-driven measurement of quantitative
features of the signal.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Olivier
full_name: Lebeltel, Olivier
last_name: Lebeltel
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Dogan
full_name: Ulus, Dogan
last_name: Ulus
citation:
ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and
quantitative trace analysis with extended signal temporal logic. In: Beyer D,
Huisman M, eds. Vol 10806. Springer; 2018:303-319. doi:10.1007/978-3-319-89963-3_18'
apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2018).
AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal
logic. In D. Beyer & M. Huisman (Eds.) (Vol. 10806, pp. 303–319). Presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89963-3_18'
chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan
Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal
Temporal Logic.” edited by Dirk Beyer and Marieke Huisman, 10806:303–19. Springer,
2018. https://doi.org/10.1007/978-3-319-89963-3_18.'
ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
Thessaloniki, Greece, 2018, vol. 10806, pp. 303–319.'
ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2018. AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10806,
303–319.'
mla: 'Nickovic, Dejan, et al. AMT 2.0: Qualitative and Quantitative Trace Analysis
with Extended Signal Temporal Logic. Edited by Dirk Beyer and Marieke Huisman,
vol. 10806, Springer, 2018, pp. 303–19, doi:10.1007/978-3-319-89963-3_18.'
short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M.
Huisman (Eds.), Springer, 2018, pp. 303–319.
conference:
end_date: 2018-04-20
location: Thessaloniki, Greece
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2018-04-14
date_created: 2018-12-11T11:45:41Z
date_published: 2018-04-14T00:00:00Z
date_updated: 2023-09-08T11:52:02Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-89963-3_18
editor:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Marieke
full_name: Huisman, Marieke
last_name: Huisman
external_id:
isi:
- '00445822600018'
file:
- access_level: open_access
checksum: e11db3b9c8e27a1c7d1c738cc5e4d25a
content_type: application/pdf
creator: dernst
date_created: 2019-02-06T07:33:05Z
date_updated: 2020-07-14T12:45:58Z
file_id: '5928'
file_name: 2018_LNCS_Nickovic.pdf
file_size: 3267209
relation: main_file
file_date_updated: 2020-07-14T12:45:58Z
has_accepted_license: '1'
intvolume: ' 10806'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 303 - 319
publication_status: published
publisher: Springer
publist_id: '7582'
quality_controlled: '1'
related_material:
record:
- id: '10861'
relation: later_version
status: public
scopus_import: '1'
status: public
title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal
temporal logic'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10806
year: '2018'
...
---
_id: '5411'
abstract:
- lang: eng
text: "Model-based testing is a promising technology for black-box software and
hardware testing, in which test cases are generated automatically from high-level
specifications. Nowadays, systems typically consist of multiple interacting components
and, due to their complexity, testing presents a considerable portion of the effort
and cost in the design process. Exploiting the compositional structure of system
specifications can considerably reduce the effort in model-based testing. Moreover,
inferring properties about the system from testing its individual components allows
the designer to reduce the amount of integration testing.\r\nIn this paper, we
study compositional properties of the IOCO-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the IOCO conformance relation, the resulting methodology
can be applied to a broader class of systems."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications
for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1
apa: Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications
for IOCO testing. IST Austria, 2014.
ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing, IST Austria, 20p.
mla: Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing.
IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications
for IOCO Testing, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-28T00:00:00Z
date_updated: 2023-02-23T10:31:07Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-148-v2-1
file:
- access_level: open_access
checksum: 0e03aba625cc334141a3148432aa5760
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:21Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5543'
file_name: IST-2014-148-v2+1_main_tr.pdf
file_size: 534732
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '152'
related_material:
record:
- id: '2167'
relation: later_version
status: public
status: public
title: Compositional specifications for IOCO testing
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '2942'
abstract:
- lang: eng
text: Interface theories provide a formal framework for component-based development
of software and hardware which supports the incremental design of systems and
the independent implementability of components. These capabilities are ensured
through mathematical properties of the parallel composition operator and the refinement
relation for components. More recently, a conjunction operation was added to interface
theories in order to provide support for handling multiple viewpoints, requirements
engineering, and component reuse. Unfortunately, the conjunction operator does
not allow independent implementability in general. In this paper, we study conditions
that need to be imposed on interface models in order to enforce independent implementability
with respect to conjunction. We focus on multiple viewpoint specifications and
propose a new compatibility criterion between two interfaces, which we call orthogonality.
We show that orthogonal interfaces can be refined separately, while preserving
both orthogonality and composability with other interfaces. We illustrate the
independent implementability of different viewpoints with a FIFO buffer example.
acknowledgement: ERC Advanced Grant QUAREM (Quantitative Reactive Modeling), FWF National
Research Network RISE (Rigorous Systems Engineering)
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Henzinger TA, Nickovic D. Independent implementability of viewpoints. In:
Conference Proceedings Monterey Workshop 2012. Vol 7539. Springer; 2012:380-395.
doi:10.1007/978-3-642-34059-8_20'
apa: 'Henzinger, T. A., & Nickovic, D. (2012). Independent implementability
of viewpoints. In Conference proceedings Monterey Workshop 2012 (Vol.
7539, pp. 380–395). Oxford, UK: Springer. https://doi.org/10.1007/978-3-642-34059-8_20'
chicago: Henzinger, Thomas A, and Dejan Nickovic. “Independent Implementability
of Viewpoints.” In Conference Proceedings Monterey Workshop 2012, 7539:380–95.
Springer, 2012. https://doi.org/10.1007/978-3-642-34059-8_20.
ieee: T. A. Henzinger and D. Nickovic, “Independent implementability of viewpoints,”
in Conference proceedings Monterey Workshop 2012, Oxford, UK, 2012, vol.
7539, pp. 380–395.
ista: Henzinger TA, Nickovic D. 2012. Independent implementability of viewpoints. Conference
proceedings Monterey Workshop 2012. Monterey Workshop 2012, LNCS, vol. 7539, 380–395.
mla: Henzinger, Thomas A., and Dejan Nickovic. “Independent Implementability of
Viewpoints.” Conference Proceedings Monterey Workshop 2012, vol. 7539,
Springer, 2012, pp. 380–95, doi:10.1007/978-3-642-34059-8_20.
short: T.A. Henzinger, D. Nickovic, in:, Conference Proceedings Monterey Workshop
2012, Springer, 2012, pp. 380–395.
conference:
end_date: 2012-03-21
location: Oxford, UK
name: Monterey Workshop 2012
start_date: 2012-03-19
date_created: 2018-12-11T12:00:28Z
date_published: 2012-09-16T00:00:00Z
date_updated: 2021-01-12T07:39:56Z
day: '16'
department:
- _id: ToHe
doi: 10.1007/978-3-642-34059-8_20
ec_funded: 1
intvolume: ' 7539'
language:
- iso: eng
month: '09'
oa_version: None
page: 380 - 395
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: ' Conference proceedings Monterey Workshop 2012'
publication_status: published
publisher: Springer
publist_id: '3791'
quality_controlled: '1'
scopus_import: 1
status: public
title: Independent implementability of viewpoints
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7539
year: '2012'
...
---
_id: '3155'
abstract:
- lang: eng
text: 'We propose synchronous interfaces, a new interface theory for discrete-time
systems. We use an application to time-triggered scheduling to drive the design
choices for our formalism; in particular, additionally to deriving useful mathematical
properties, we focus on providing a syntax which is adapted to natural high-level
system modeling. As a result, we develop an interface model that relies on a guarded-command
based language and is equipped with shared variables and explicit discrete-time
clocks. We define all standard interface operations: compatibility checking, composition,
refinement, and shared refinement. Apart from the synchronous interface model,
the contribution of this paper is the establishment of a formal relation between
interface theories and real-time scheduling, where we demonstrate a fully automatic
framework for the incremental computation of time-triggered schedules.'
acknowledgement: Research partially supported by the Danish-Chinese Center for Cyber
Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.
alternative_title:
- LNCS
author:
- first_name: Benoît
full_name: Delahaye, Benoît
last_name: Delahaye
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface
theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218.
doi:10.1007/978-3-642-30793-5_13'
apa: 'Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., & Nickovic,
D. (2012). Synchronous interface theories and time triggered scheduling (Vol.
7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and
Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed
Systems , Stockholm, Sweden: Springer. https://doi.org/10.1007/978-3-642-30793-5_13'
chicago: Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan
Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18.
Springer, 2012. https://doi.org/10.1007/978-3-642-30793-5_13.
ieee: 'B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous
interface theories and time triggered scheduling,” presented at the FORTE: Formal
Techniques for Networked and Distributed Systems & FMOODS: Formal Methods
for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273,
pp. 203–218.'
ista: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous
interface theories and time triggered scheduling. FORTE: Formal Techniques for
Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based
Distributed Systems , LNCS, vol. 7273, 203–218.'
mla: Delahaye, Benoît, et al. Synchronous Interface Theories and Time Triggered
Scheduling. Vol. 7273, Springer, 2012, pp. 203–18, doi:10.1007/978-3-642-30793-5_13.
short: B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer,
2012, pp. 203–218.
conference:
end_date: 2012-06-16
location: Stockholm, Sweden
name: 'FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS:
Formal Methods for Open Object-Based Distributed Systems '
start_date: 2012-06-13
date_created: 2018-12-11T12:01:43Z
date_published: 2012-06-01T00:00:00Z
date_updated: 2021-01-12T07:41:26Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-30793-5_13
file:
- access_level: open_access
checksum: feae2e07f2d9a59843f8ddabf25d179f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:25Z
date_updated: 2020-07-14T12:46:01Z
file_id: '4879'
file_name: IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf
file_size: 493198
relation: main_file
file_date_updated: 2020-07-14T12:46:01Z
has_accepted_license: '1'
intvolume: ' 7273'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 203 - 218
publication_status: published
publisher: Springer
publist_id: '3539'
pubrep_id: '88'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synchronous interface theories and time triggered scheduling
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7273
year: '2012'
...
---
_id: '3162'
abstract:
- lang: eng
text: Given a dense-time real-valued signal and a parameterized temporal logic formula
with both magnitude and timing parameters, we compute the subset of the parameter
space that renders the formula satisfied by the trace. We provide two preliminary
implementations, one which follows the exact semantics and attempts to compute
the validity domain by quantifier elimination in linear arithmetics and one which
conducts adaptive search in the parameter space.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Eugene
full_name: Asarin, Eugene
last_name: Asarin
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Asarin E, Donzé A, Maler O, Nickovic D. Parametric identification of temporal
properties. In: Vol 7186. Springer; 2012:147-160. doi:10.1007/978-3-642-29860-8_12'
apa: 'Asarin, E., Donzé, A., Maler, O., & Nickovic, D. (2012). Parametric identification
of temporal properties (Vol. 7186, pp. 147–160). Presented at the RV: Runtime
Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-642-29860-8_12'
chicago: Asarin, Eugene, Alexandre Donzé, Oded Maler, and Dejan Nickovic. “Parametric
Identification of Temporal Properties,” 7186:147–60. Springer, 2012. https://doi.org/10.1007/978-3-642-29860-8_12.
ieee: 'E. Asarin, A. Donzé, O. Maler, and D. Nickovic, “Parametric identification
of temporal properties,” presented at the RV: Runtime Verification, San Francisco,
CA, United States, 2012, vol. 7186, pp. 147–160.'
ista: 'Asarin E, Donzé A, Maler O, Nickovic D. 2012. Parametric identification of
temporal properties. RV: Runtime Verification, LNCS, vol. 7186, 147–160.'
mla: Asarin, Eugene, et al. Parametric Identification of Temporal Properties.
Vol. 7186, Springer, 2012, pp. 147–60, doi:10.1007/978-3-642-29860-8_12.
short: E. Asarin, A. Donzé, O. Maler, D. Nickovic, in:, Springer, 2012, pp. 147–160.
conference:
end_date: 2011-09-30
location: San Francisco, CA, United States
name: 'RV: Runtime Verification'
start_date: 2011-09-27
date_created: 2018-12-11T12:01:45Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2021-01-12T07:41:29Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-29860-8_12
file:
- access_level: open_access
checksum: ba4a75287008fc64b8fbf78a7476ec32
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T12:50:15Z
date_updated: 2020-07-14T12:46:01Z
file_id: '7862'
file_name: 2012_RV_Asarin.pdf
file_size: 374726
relation: main_file
file_date_updated: 2020-07-14T12:46:01Z
has_accepted_license: '1'
intvolume: ' 7186'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 147 - 160
publication_status: published
publisher: Springer
publist_id: '3525'
quality_controlled: '1'
scopus_import: 1
status: public
title: Parametric identification of temporal properties
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7186
year: '2012'
...
---
_id: '3362'
abstract:
- lang: eng
text: State-transition systems communicating by shared variables have been the underlying
model of choice for applications of model checking. Such formalisms, however,
have difficulty with modeling process creation or death and communication reconfigurability.
Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling
formalism that supports dynamic reconfiguration and creation/death of processes.
The resulting formalism supports two types of variables, data variables and reference
variables. Reference variables enable changing the connectivity between processes
and referring to instances of processes. We show how this new formalism supports
parallel composition and refinement through trace containment. DRM provide a natural
language for modeling (and ultimately reasoning about) biological systems and
multiple threads communicating through shared variables.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
- first_name: Anmol
full_name: Singh, Anmol
last_name: Singh
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. Dynamic
reactive modules. In: Vol 6901. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2011:404-418. doi:10.1007/978-3-642-23217-6_27'
apa: 'Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., &
Vardi, M. (2011). Dynamic reactive modules (Vol. 6901, pp. 404–418). Presented
at the CONCUR: Concurrency Theory, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/978-3-642-23217-6_27'
chicago: Fisher, Jasmin, Thomas A Henzinger, Dejan Nickovic, Nir Piterman, Anmol
Singh, and Moshe Vardi. “Dynamic Reactive Modules,” 6901:404–18. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2011. https://doi.org/10.1007/978-3-642-23217-6_27.
ieee: 'J. Fisher, T. A. Henzinger, D. Nickovic, N. Piterman, A. Singh, and M. Vardi,
“Dynamic reactive modules,” presented at the CONCUR: Concurrency Theory, Aachen,
Germany, 2011, vol. 6901, pp. 404–418.'
ista: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. 2011. Dynamic
reactive modules. CONCUR: Concurrency Theory, LNCS, vol. 6901, 404–418.'
mla: Fisher, Jasmin, et al. Dynamic Reactive Modules. Vol. 6901, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:10.1007/978-3-642-23217-6_27.
short: J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, A. Singh, M. Vardi,
in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–418.
conference:
end_date: 2011-09-09
location: Aachen, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2011-09-06
date_created: 2018-12-11T12:02:54Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-23217-6_27
ec_funded: 1
file:
- access_level: open_access
checksum: 6bf2453d8e52e979ddb58d17325bad26
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:17:48Z
date_updated: 2020-07-14T12:46:10Z
file_id: '7870'
file_name: 2011_CONCUR_Fisher.pdf
file_size: 337125
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6901'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 404 - 418
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '3253'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dynamic reactive modules
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6901
year: '2011'
...
---
_id: '4369'
abstract:
- lang: eng
text: In this paper we propose a novel technique for constructing timed automata
from properties expressed in the logic mtl, under bounded-variability assumptions.
We handle full mtl and include all future operators. Our construction is based
on separation of the continuous time monitoring of the input sequence and discrete
predictions regarding the future. The separation of the continuous from the discrete
allows us to determinize our automata in an exponential construction that does
not increase the number of clocks. This leads to a doubly exponential construction
from mtl to deterministic timed automata, compared with triply exponential using
existing approaches. We offer an alternative to the existing approach to linear
real-time model checking, which has never been implemented. It further offers
a unified framework for model checking, runtime monitoring, and synthesis, in
an approach that can reuse tools, implementations, and insights from the discrete
setting.
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Nickovic D, Piterman N. From MTL to deterministic timed automata. In: Henzinger
TA, Chatterjee K, eds. Vol 6246. Springer; 2010:152-167. doi:10.1007/978-3-642-15297-9_13'
apa: 'Nickovic, D., & Piterman, N. (2010). From MTL to deterministic timed automata.
In T. A. Henzinger & K. Chatterjee (Eds.) (Vol. 6246, pp. 152–167). Presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria: Springer. https://doi.org/10.1007/978-3-642-15297-9_13'
chicago: Nickovic, Dejan, and Nir Piterman. “From MTL to Deterministic Timed Automata.”
edited by Thomas A. Henzinger and Krishnendu Chatterjee, 6246:152–67. Springer,
2010. https://doi.org/10.1007/978-3-642-15297-9_13.
ieee: 'D. Nickovic and N. Piterman, “From MTL to deterministic timed automata,”
presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria, 2010, vol. 6246, pp. 152–167.'
ista: 'Nickovic D, Piterman N. 2010. From MTL to deterministic timed automata. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 6246, 152–167.'
mla: Nickovic, Dejan, and Nir Piterman. From MTL to Deterministic Timed Automata.
Edited by Thomas A. Henzinger and Krishnendu Chatterjee, vol. 6246, Springer,
2010, pp. 152–67, doi:10.1007/978-3-642-15297-9_13.
short: D. Nickovic, N. Piterman, in:, T.A. Henzinger, K. Chatterjee (Eds.), Springer,
2010, pp. 152–167.
conference:
end_date: 2010-09-10
location: Klosterneuburg, Austria
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2010-09-08
date_created: 2018-12-11T12:08:30Z
date_published: 2010-09-08T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '08'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15297-9_13
ec_funded: 1
editor:
- first_name: Thomas A.
full_name: Henzinger, Thomas A.
last_name: Henzinger
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
last_name: Chatterjee
file:
- access_level: open_access
checksum: b0ca5f5fbe8a3d20ccbc6f51a344a459
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:43Z
date_updated: 2020-07-14T12:46:27Z
file_id: '5028'
file_name: IST-2012-49-v1+1_From_MTL_to_deterministic_timed_automata.pdf
file_size: 249789
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
intvolume: ' 6246'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 152 - 167
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '1090'
pubrep_id: '49'
quality_controlled: '1'
scopus_import: 1
status: public
title: From MTL to deterministic timed automata
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6246
year: '2010'
...
---
_id: '4379'
abstract:
- lang: eng
text: |
The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be interfaced with a simulator and alert the user if the property is violated by a simulation trace. Although not complete, this lighter approach to formal verification has been effectively used in software and digital hardware to detect errors. Recently, the idea of property checkers has been extended to analog and mixed-signal systems.
In this paper, we apply the property-based checking methodology to an industrial and realistic example of a DDR2 memory interface. The properties describing the DDR2 analog behavior are expressed in the formal specification language stl/psl in form of assertions. The simulation traces generated from an actual DDR2 interface design are checked with respect to the stl/psl assertions using the amt tool. The focus of this paper is on the translation of the official (informal and descriptive) specification of two non-trivial DDR2 properties into stl/psl assertions. We study both the benefits and the current limits of such approach.
acknowledgement: We would like to thank Tom Giovannini from Rambus, Inc. for his detailed
explana- tions of the DDR2 specification and for providing us with simulation traces.
We would also like to thank Oded Maler from Verimag for discussions on the STL/PSL
language and its extensions.
author:
- first_name: Kevin
full_name: Jones, Kevin D
last_name: Jones
- first_name: Victor
full_name: Konrad,Victor
last_name: Konrad
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Jones K, Konrad V, Nickovic D. Analog property checkers: a DDR2 case study.
Formal Methods in System Design. 2010;36(2):114-130. doi:10.1007/s10703-009-0085-x'
apa: 'Jones, K., Konrad, V., & Nickovic, D. (2010). Analog property checkers:
a DDR2 case study. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-009-0085-x'
chicago: 'Jones, Kevin, Victor Konrad, and Dejan Nickovic. “Analog Property Checkers:
A DDR2 Case Study.” Formal Methods in System Design. Springer, 2010. https://doi.org/10.1007/s10703-009-0085-x.'
ieee: 'K. Jones, V. Konrad, and D. Nickovic, “Analog property checkers: a DDR2 case
study,” Formal Methods in System Design, vol. 36, no. 2. Springer, pp.
114–130, 2010.'
ista: 'Jones K, Konrad V, Nickovic D. 2010. Analog property checkers: a DDR2 case
study. Formal Methods in System Design. 36(2), 114–130.'
mla: 'Jones, Kevin, et al. “Analog Property Checkers: A DDR2 Case Study.” Formal
Methods in System Design, vol. 36, no. 2, Springer, 2010, pp. 114–30, doi:10.1007/s10703-009-0085-x.'
short: K. Jones, V. Konrad, D. Nickovic, Formal Methods in System Design 36 (2010)
114–130.
date_created: 2018-12-11T12:08:33Z
date_published: 2010-06-01T00:00:00Z
date_updated: 2021-01-12T07:56:31Z
day: '01'
doi: 10.1007/s10703-009-0085-x
extern: 1
intvolume: ' 36'
issue: '2'
main_file_link:
- open_access: '1'
url: http://openaccess.city.ac.uk/1066/
month: '06'
oa: 1
page: 114 - 130
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '1080'
quality_controlled: 0
status: public
title: 'Analog property checkers: a DDR2 case study'
type: journal_article
volume: 36
year: '2010'
...
---
_id: '4389'
abstract:
- lang: eng
text: 'Digital components play a central role in the design of complex embedded
systems. These components are interconnected with other, possibly analog, devices
and the physical environment. This environment cannot be entirely captured and
can provide inaccurate input data to the component. It is thus important for digital
components to have a robust behavior, i.e. the presence of a small change in the
input sequences should not result in a drastic change in the output sequences.
In this paper, we study a notion of robustness for sequential circuits. However,
since sequential circuits may have parts that are naturally discontinuous (e.g.,
digital controllers with switching behavior), we need a flexible framework that
accommodates this fact and leaves discontinuous parts of the circuit out from
the robustness analysis. As a consequence, we consider sequential circuits that
have their input variables partitioned into two disjoint sets: control and disturbance
variables. Our contributions are (1) a definition of robustness for sequential
circuits as a form of continuity with respect to disturbance variables, (2) the
characterization of the exact class of sequential circuits that are robust according
to our definition, (3) an algorithm to decide whether a sequential circuit is
robust or not.'
author:
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Doyen L, Henzinger TA, Legay A, Nickovic D. Robustness of sequential circuits.
In: IEEE; 2010:77-84. doi:10.1109/ACSD.2010.26'
apa: 'Doyen, L., Henzinger, T. A., Legay, A., & Nickovic, D. (2010). Robustness
of sequential circuits (pp. 77–84). Presented at the ACSD: Application of Concurrency
to System Design, IEEE. https://doi.org/10.1109/ACSD.2010.26'
chicago: Doyen, Laurent, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Robustness
of Sequential Circuits,” 77–84. IEEE, 2010. https://doi.org/10.1109/ACSD.2010.26.
ieee: 'L. Doyen, T. A. Henzinger, A. Legay, and D. Nickovic, “Robustness of sequential
circuits,” presented at the ACSD: Application of Concurrency to System Design,
2010, pp. 77–84.'
ista: 'Doyen L, Henzinger TA, Legay A, Nickovic D. 2010. Robustness of sequential
circuits. ACSD: Application of Concurrency to System Design, 77–84.'
mla: Doyen, Laurent, et al. Robustness of Sequential Circuits. IEEE, 2010,
pp. 77–84, doi:10.1109/ACSD.2010.26.
short: L. Doyen, T.A. Henzinger, A. Legay, D. Nickovic, in:, IEEE, 2010, pp. 77–84.
conference:
name: 'ACSD: Application of Concurrency to System Design'
date_created: 2018-12-11T12:08:36Z
date_published: 2010-08-23T00:00:00Z
date_updated: 2021-01-12T07:56:36Z
day: '23'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/ACSD.2010.26
file:
- access_level: open_access
checksum: 42b2952bfc6b6974617bd554842b904a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:10Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4733'
file_name: IST-2012-44-v1+1_Robustness_of_sequential_circuits.pdf
file_size: 159920
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 77 - 84
publication_status: published
publisher: IEEE
publist_id: '1069'
pubrep_id: '44'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness of sequential circuits
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4371'
abstract:
- lang: eng
text: We survey some of the problems associated with checking whether a given behavior
(a sequence, a Boolean signal or a continuous signal) satisfies a property specified
in an appropriate temporal logic and describe two such monitoring algorithms for
the real-time logic MITL.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. Checking Temporal Properties of Discrete, Timed
and Continuous Behaviors. In: Pillars of Computer Science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. Springer;
2008:475-505. doi:10.1007/978-3-540-78127-1_26'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2008). Checking Temporal Properties
of Discrete, Timed and Continuous Behaviors. In Pillars of Computer science:
Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday
(pp. 475–505). Springer. https://doi.org/10.1007/978-3-540-78127-1_26'
chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Checking Temporal Properties
of Discrete, Timed and Continuous Behaviors.” In Pillars of Computer Science:
Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday,
475–505. Springer, 2008. https://doi.org/10.1007/978-3-540-78127-1_26.'
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Checking Temporal Properties of Discrete,
Timed and Continuous Behaviors,” in Pillars of Computer science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer,
2008, pp. 475–505.'
ista: 'Maler O, Nickovic D, Pnueli A. 2008.Checking Temporal Properties of Discrete,
Timed and Continuous Behaviors. In: Pillars of Computer science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. LNCS, , 475–505.'
mla: 'Maler, Oded, et al. “Checking Temporal Properties of Discrete, Timed and Continuous
Behaviors.” Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot
on the Occasion of His 85th Birthday, Springer, 2008, pp. 475–505, doi:10.1007/978-3-540-78127-1_26.'
short: 'O. Maler, D. Nickovic, A. Pnueli, in:, Pillars of Computer Science: Essays
Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer,
2008, pp. 475–505.'
date_created: 2018-12-11T12:08:30Z
date_published: 2008-03-11T00:00:00Z
date_updated: 2023-02-14T10:42:38Z
day: '11'
doi: 10.1007/978-3-540-78127-1_26
extern: '1'
language:
- iso: eng
month: '03'
oa_version: None
page: 475 - 505
publication: 'Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot
on the Occasion of His 85th Birthday'
publication_identifier:
isbn:
- '9783540781264'
publication_status: published
publisher: Springer
publist_id: '1087'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '4368'
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
citation:
ama: 'Nickovic D, Maler O. AMT: a property-based monitoring tool for analog systems.
In: Springer; 2007:304-319. doi:1567'
apa: 'Nickovic, D., & Maler, O. (2007). AMT: a property-based monitoring tool
for analog systems (pp. 304–319). Presented at the FORMATS: Formal Modeling and
Analysis of Timed Systems, Springer. https://doi.org/1567'
chicago: 'Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool
for Analog Systems,” 304–19. Springer, 2007. https://doi.org/1567.'
ieee: 'D. Nickovic and O. Maler, “AMT: a property-based monitoring tool for analog
systems,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems,
2007, pp. 304–319.'
ista: 'Nickovic D, Maler O. 2007. AMT: a property-based monitoring tool for analog
systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 304–319.'
mla: 'Nickovic, Dejan, and Oded Maler. AMT: A Property-Based Monitoring Tool
for Analog Systems. Springer, 2007, pp. 304–19, doi:1567.'
short: D. Nickovic, O. Maler, in:, Springer, 2007, pp. 304–319.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '20'
doi: '1567'
extern: 1
month: '09'
page: 304 - 319
publication_status: published
publisher: Springer
publist_id: '1089'
quality_controlled: 0
status: public
title: 'AMT: a property-based monitoring tool for analog systems'
type: conference
year: '2007'
...
---
_id: '4370'
alternative_title:
- Lecture Notes in Computer Science
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. On synthesizing controllers from bounded-response
properties. In: Springer; 2007:95-107. doi:1568'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers
from bounded-response properties (pp. 95–107). Presented at the CAV: Computer
Aided Verification, Springer. https://doi.org/1568'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers
from Bounded-Response Properties,” 95–107. Springer, 2007. https://doi.org/1568.
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “On synthesizing controllers from bounded-response
properties,” presented at the CAV: Computer Aided Verification, 2007, pp. 95–107.'
ista: 'Maler O, Nickovic D, Pnueli A. 2007. On synthesizing controllers from bounded-response
properties. CAV: Computer Aided Verification, Lecture Notes in Computer Science,
, 95–107.'
mla: Maler, Oded, et al. On Synthesizing Controllers from Bounded-Response Properties.
Springer, 2007, pp. 95–107, doi:1568.
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2007, pp. 95–107.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:28Z
day: '01'
doi: '1568'
extern: 1
month: '01'
page: 95 - 107
publication_status: published
publisher: Springer
publist_id: '1086'
quality_controlled: 0
status: public
title: On synthesizing controllers from bounded-response properties
type: conference
year: '2007'
...
---
_id: '4373'
alternative_title:
- LNCS
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. Real Time Temporal Logic: Past, Present, Future.
In: Springer; 2006:2-16. doi:1571'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). Real Time Temporal Logic:
Past, Present, Future (pp. 2–16). Presented at the FORMATS: Formal Modeling and
Analysis of Timed Systems, Springer. https://doi.org/1571'
chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Real Time Temporal Logic:
Past, Present, Future,” 2–16. Springer, 2006. https://doi.org/1571.'
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Real Time Temporal Logic: Past, Present,
Future,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems,
2006, pp. 2–16.'
ista: 'Maler O, Nickovic D, Pnueli A. 2006. Real Time Temporal Logic: Past, Present,
Future. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 2–16.'
mla: 'Maler, Oded, et al. Real Time Temporal Logic: Past, Present, Future.
Springer, 2006, pp. 2–16, doi:1571.'
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 2–16.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2006-01-23T00:00:00Z
date_updated: 2021-01-12T07:56:29Z
day: '23'
doi: '1571'
extern: 1
month: '01'
page: 2 - 16
publication_status: published
publisher: Springer
publist_id: '1084'
quality_controlled: 0
status: public
title: 'Real Time Temporal Logic: Past, Present, Future'
type: conference
year: '2006'
...
---
_id: '4374'
alternative_title:
- LNCS
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. From MITL to Timed Automata. In: Springer;
2006:274-289. doi:1570'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). From MITL to Timed Automata
(pp. 274–289). Presented at the FORMATS: Formal Modeling and Analysis of Timed
Systems, Springer. https://doi.org/1570'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “From MITL to Timed Automata,”
274–89. Springer, 2006. https://doi.org/1570.
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “From MITL to Timed Automata,” presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, pp. 274–289.'
ista: 'Maler O, Nickovic D, Pnueli A. 2006. From MITL to Timed Automata. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, , 274–289.'
mla: Maler, Oded, et al. From MITL to Timed Automata. Springer, 2006, pp.
274–89, doi:1570.
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 274–289.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2006-10-19T00:00:00Z
date_updated: 2021-01-12T07:56:30Z
day: '19'
doi: '1570'
extern: 1
month: '10'
page: 274 - 289
publication_status: published
publisher: Springer
publist_id: '1085'
quality_controlled: 0
status: public
title: From MITL to Timed Automata
type: conference
year: '2006'
...