[{"external_id":{"arxiv":["2305.02836"]},"year":"2023","date_published":"2023-09-01T00:00:00Z","conference":{"start_date":"2023-09-19","end_date":"2023-09-22","name":"CONCUR: Conference on Concurrency Theory","location":"Antwerp, Belgium"},"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.","ec_funded":1,"status":"public","publication":"34th International Conference on Concurrency Theory","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"type":"conference","_id":"14405","date_updated":"2023-10-09T07:43:44Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_processing_charge":"Yes","alternative_title":["LIPIcs"],"doi":"10.4230/LIPIcs.CONCUR.2023.21","quality_controlled":"1","ddc":["000"],"article_number":"21","file":[{"checksum":"215765e40454d806174ac0a223e8d6fa","relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2023_LIPcs_Bartocci.pdf","file_id":"14413","date_updated":"2023-10-09T07:42:45Z","creator":"dernst","file_size":795790,"date_created":"2023-10-09T07:42:45Z"}],"department":[{"_id":"ToHe"}],"arxiv":1,"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">10.4230/LIPIcs.CONCUR.2023.21</a>","ieee":"E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279.","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.","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.","chicago":"Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>.","apa":"Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2023). Hypernode automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">10.4230/LIPIcs.CONCUR.2023.21</a>."},"language":[{"iso":"eng"}],"oa":1,"date_created":"2023-10-08T22:01:16Z","volume":279,"title":"Hypernode automata","oa_version":"Published Version","scopus_import":"1","day":"01","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"orcid":"0000-0002-8741-5799","first_name":"Ana","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4"}],"file_date_updated":"2023-10-09T07:42:45Z","publication_status":"published","publication_identifier":{"issn":["18688969"],"isbn":["9783959772990"]},"intvolume":"       279","license":"https://creativecommons.org/licenses/by/4.0/","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1"},{"author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira","last_name":"Da Costa"}],"day":"14","scopus_import":"1","oa_version":"Preprint","title":"Flavors of sequential information flow","volume":13182,"date_created":"2022-02-20T23:01:34Z","intvolume":"     13182","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."}],"publication_status":"published","publication_identifier":{"issn":["03029743"],"isbn":["9783030945824"],"eissn":["16113349"]},"month":"01","arxiv":1,"department":[{"_id":"ToHe"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential information flow. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 13182. Springer Nature; 2022:1-19. doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Flavors of sequential information flow,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Philadelphia, PA, United States, 2022, vol. 13182, pp. 1–19.","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.","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.","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 13182:1–19. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>.","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Flavors of sequential information flow. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 13182, pp. 1–19). Philadelphia, PA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>","mla":"Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 13182, Springer Nature, 2022, pp. 1–19, doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-030-94583-1_1","alternative_title":["LNCS"],"article_processing_charge":"No","publisher":"Springer Nature","date_updated":"2022-08-05T09:02:56Z","_id":"10774","type":"conference","page":"1-19","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2105.02013","open_access":"1"}],"quality_controlled":"1","year":"2022","external_id":{"arxiv":["2105.02013"]},"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","status":"public","date_published":"2022-01-14T00:00:00Z","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.","conference":{"name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","end_date":"2022-01-18","start_date":"2022-01-16","location":"Philadelphia, PA, United States"}},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>.","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Information-flow interfaces. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In <i>Fundamental Approaches to Software Engineering</i>, 13241:3–22. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>.","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.","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.","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in <i>Fundamental Approaches to Software Engineering</i>, Munich, Germany, 2022, vol. 13241, pp. 3–22.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13241. Springer Nature; 2022:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>"},"language":[{"iso":"eng"}],"oa":1,"file":[{"relation":"main_file","checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","file_name":"2022_LNCS_Bartocci.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","file_id":"11357","date_created":"2022-05-09T06:52:44Z","file_size":479146,"creator":"dernst","date_updated":"2022-05-09T06:52:44Z"}],"department":[{"_id":"ToHe"}],"month":"03","file_date_updated":"2022-05-09T06:52:44Z","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030994280"],"eissn":["1611-3349"]},"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"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."}],"intvolume":"     13241","has_accepted_license":"1","date_created":"2022-05-08T22:01:44Z","volume":13241,"title":"Information-flow interfaces","oa_version":"Published Version","day":"29","scopus_import":"1","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Da Costa, Ana Oliveira","last_name":"Da Costa","first_name":"Ana Oliveira"}],"conference":{"location":"Munich, Germany","end_date":"2022-04-07","start_date":"2022-04-02","name":"FASE: Fundamental Approaches to Software Engineering"},"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.","date_published":"2022-03-29T00:00:00Z","ec_funded":1,"status":"public","publication":"Fundamental Approaches to Software Engineering","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"external_id":{"isi":["000782393600001"]},"isi":1,"year":"2022","quality_controlled":"1","ddc":["000"],"page":"3-22","type":"conference","_id":"11355","date_updated":"2023-08-03T07:03:40Z","publisher":"Springer Nature","article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-99429-7_1"},{"publication":"International Journal on Software Tools for Technology Transfer","status":"public","date_published":"2020-08-03T00:00:00Z","external_id":{"isi":["000555398600001"]},"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"299"}]},"year":"2020","isi":1,"keyword":["Information Systems","Software"],"page":"741-758","quality_controlled":"1","publisher":"Springer Nature","doi":"10.1007/s10009-020-00582-z","article_processing_charge":"No","type":"journal_article","date_updated":"2023-09-08T11:52:02Z","_id":"10861","language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"6","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. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","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,” <i>International Journal on Software Tools for Technology Transfer</i>, 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.","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.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>"},"month":"08","department":[{"_id":"ToHe"}],"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."}],"intvolume":"        22","publication_status":"published","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"oa_version":"None","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","author":[{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"first_name":"Olivier","last_name":"Lebeltel","full_name":"Lebeltel, Olivier"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"full_name":"Ulus, Dogan","last_name":"Ulus","first_name":"Dogan"}],"scopus_import":"1","day":"03","article_type":"original","date_created":"2022-03-18T10:10:53Z","volume":22},{"month":"08","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"citation":{"ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","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.","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:59-75. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>","apa":"Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal logic. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>","mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>.","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.","chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"}],"day":"13","scopus_import":"1","oa_version":"None","title":"Mixed-time signal temporal logic","volume":11750,"date_created":"2020-01-05T23:00:48Z","intvolume":"     11750","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. "}],"publication_status":"published","publication_identifier":{"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"],"eissn":["1611-3349"]},"isi":1,"year":"2019","external_id":{"isi":["000611677700004"]},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"status":"public","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","conference":{"name":"FORMATS: Formal Modeling and Anaysis of Timed Systems","start_date":"2019-08-27","end_date":"2019-08-29","location":"Amsterdam, The Netherlands"},"date_published":"2019-08-13T00:00:00Z","doi":"10.1007/978-3-030-29662-9_4","article_processing_charge":"No","alternative_title":["LNCS"],"publisher":"Springer Nature","date_updated":"2023-09-06T14:57:17Z","_id":"7232","type":"conference","page":"59-75","quality_controlled":"1"},{"publication_identifier":{"isbn":["9781450362825"]},"publication_status":"published","file_date_updated":"2020-10-08T17:25:45Z","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","date_created":"2019-05-13T08:13:46Z","oa_version":"Submitted Version","title":"Interface-aware signal temporal logic","author":[{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"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é"},{"last_name":"Ito","full_name":"Ito, Hisahiro","first_name":"Hisahiro"},{"full_name":"Kapinski, James","last_name":"Kapinski","first_name":"James"}],"day":"16","scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"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>.","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>.","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>","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>","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.","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."},"language":[{"iso":"eng"}],"oa":1,"file":[{"date_created":"2020-10-08T17:25:45Z","file_size":1055421,"creator":"dernst","date_updated":"2020-10-08T17:25:45Z","file_id":"8633","file_name":"2019_ACM_Ferrere.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"b8e967081e051d1c55ca5d18fb187890"}],"department":[{"_id":"ToHe"}],"month":"04","quality_controlled":"1","ddc":["000"],"page":"57-66","type":"conference","date_updated":"2023-08-25T10:19:23Z","_id":"6428","publisher":"ACM","doi":"10.1145/3302504.3311800","article_processing_charge":"No","date_published":"2019-04-16T00:00:00Z","conference":{"start_date":"2019-04-16","end_date":"2019-04-18","name":"HSCC: Hybrid Systems Computation and Control","location":"Montreal, Canada"},"project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"status":"public","publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","external_id":{"isi":["000516713900007"]},"year":"2019","isi":1},{"type":"conference","_id":"299","date_updated":"2023-09-08T11:52:02Z","publisher":"Springer","editor":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"last_name":"Huisman","full_name":"Huisman, Marieke","first_name":"Marieke"}],"alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-319-89963-3_18","quality_controlled":"1","ddc":["000"],"page":"303 - 319","publist_id":"7582","related_material":{"record":[{"id":"10861","status":"public","relation":"later_version"}]},"external_id":{"isi":["00445822600018"]},"isi":1,"year":"2018","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2018-04-20","start_date":"2018-04-14","location":"Thessaloniki, Greece"},"date_published":"2018-04-14T00:00:00Z","status":"public","date_created":"2018-12-11T11:45:41Z","volume":10806,"oa_version":"Published Version","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","scopus_import":"1","day":"14","author":[{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan"},{"first_name":"Olivier","last_name":"Lebeltel","full_name":"Lebeltel, Olivier"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"first_name":"Dogan","full_name":"Ulus, Dogan","last_name":"Ulus"}],"file_date_updated":"2020-07-14T12:45:58Z","publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"     10806","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","file":[{"access_level":"open_access","content_type":"application/pdf","file_name":"2018_LNCS_Nickovic.pdf","checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","relation":"main_file","date_updated":"2020-07-14T12:45:58Z","creator":"dernst","file_size":3267209,"date_created":"2019-02-06T07:33:05Z","file_id":"5928"}],"department":[{"_id":"ToHe"}],"month":"04","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319.","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:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer &#38; 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. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>","mla":"Nickovic, Dejan, et al. <i>AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic</i>. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>.","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.","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. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>."},"language":[{"iso":"eng"}],"oa":1},{"oa":1,"status":"public","pubrep_id":"152","language":[{"iso":"eng"}],"citation":{"mla":"Daca, Przemyslaw, et al. <i>Compositional Specifications for IOCO Testing</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">10.15479/AT:IST-2014-148-v2-1</a>.","apa":"Daca, P., Henzinger, T. A., Krenn, W., &#38; Nickovic, D. (2014). <i>Compositional specifications for IOCO testing</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. <i>Compositional Specifications for IOCO Testing</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014.","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, <i>Compositional specifications for IOCO testing</i>. IST Austria, 2014.","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. <i>Compositional Specifications for IOCO Testing</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">10.15479/AT:IST-2014-148-v2-1</a>"},"date_published":"2014-01-28T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2014","month":"01","related_material":{"record":[{"id":"2167","relation":"later_version","status":"public"}]},"department":[{"_id":"ToHe"}],"file":[{"file_id":"5543","creator":"system","date_updated":"2020-07-14T12:46:46Z","date_created":"2018-12-12T11:54:21Z","file_size":534732,"checksum":"0e03aba625cc334141a3148432aa5760","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-148-v2+1_main_tr.pdf"}],"page":"20","has_accepted_license":"1","abstract":[{"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.","lang":"eng"}],"ddc":["000"],"publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","file_date_updated":"2020-07-14T12:46:46Z","doi":"10.15479/AT:IST-2014-148-v2-1","author":[{"last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Willibald","last_name":"Krenn","full_name":"Krenn, Willibald"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"}],"day":"28","alternative_title":["IST Austria Technical Report"],"title":"Compositional specifications for IOCO testing","oa_version":"Published Version","publisher":"IST Austria","date_updated":"2023-02-23T10:31:07Z","_id":"5411","type":"technical_report","date_created":"2018-12-12T11:39:11Z"},{"intvolume":"      7539","abstract":[{"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.","lang":"eng"}],"publication_status":"published","author":[{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"}],"scopus_import":1,"day":"16","oa_version":"None","title":"Independent implementability of viewpoints","volume":7539,"date_created":"2018-12-11T12:00:28Z","language":[{"iso":"eng"}],"citation":{"chicago":"Henzinger, Thomas A, and Dejan Nickovic. “Independent Implementability of Viewpoints.” In <i> Conference Proceedings Monterey Workshop 2012</i>, 7539:380–95. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-34059-8_20\">https://doi.org/10.1007/978-3-642-34059-8_20</a>.","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.” <i> Conference Proceedings Monterey Workshop 2012</i>, vol. 7539, Springer, 2012, pp. 380–95, doi:<a href=\"https://doi.org/10.1007/978-3-642-34059-8_20\">10.1007/978-3-642-34059-8_20</a>.","apa":"Henzinger, T. A., &#38; Nickovic, D. (2012). Independent implementability of viewpoints. In <i> Conference proceedings Monterey Workshop 2012</i> (Vol. 7539, pp. 380–395). Oxford, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-34059-8_20\">https://doi.org/10.1007/978-3-642-34059-8_20</a>","ama":"Henzinger TA, Nickovic D. Independent implementability of viewpoints. In: <i> Conference Proceedings Monterey Workshop 2012</i>. Vol 7539. Springer; 2012:380-395. doi:<a href=\"https://doi.org/10.1007/978-3-642-34059-8_20\">10.1007/978-3-642-34059-8_20</a>","short":"T.A. Henzinger, D. Nickovic, in:,  Conference Proceedings Monterey Workshop 2012, Springer, 2012, pp. 380–395.","ieee":"T. A. Henzinger and D. Nickovic, “Independent implementability of viewpoints,” in <i> Conference proceedings Monterey Workshop 2012</i>, Oxford, UK, 2012, vol. 7539, pp. 380–395."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"09","department":[{"_id":"ToHe"}],"page":"380 - 395","quality_controlled":"1","doi":"10.1007/978-3-642-34059-8_20","alternative_title":["LNCS"],"publisher":"Springer","date_updated":"2021-01-12T07:39:56Z","_id":"2942","type":"conference","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"status":"public","publication":" Conference proceedings Monterey Workshop 2012","ec_funded":1,"conference":{"location":"Oxford, UK","start_date":"2012-03-19","end_date":"2012-03-21","name":"Monterey Workshop 2012"},"date_published":"2012-09-16T00:00:00Z","acknowledgement":"ERC Advanced Grant QUAREM (Quantitative Reactive Modeling), FWF National Research Network RISE (Rigorous Systems Engineering)","year":"2012","publist_id":"3791"},{"file":[{"file_size":493198,"date_created":"2018-12-12T10:11:25Z","creator":"system","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","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"feae2e07f2d9a59843f8ddabf25d179f"}],"department":[{"_id":"ToHe"}],"month":"06","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"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 &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273, pp. 203–218.","short":"B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer, 2012, pp. 203–218.","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:<a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">10.1007/978-3-642-30793-5_13</a>","apa":"Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., &#38; 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 &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">https://doi.org/10.1007/978-3-642-30793-5_13</a>","mla":"Delahaye, Benoît, et al. <i>Synchronous Interface Theories and Time Triggered Scheduling</i>. Vol. 7273, Springer, 2012, pp. 203–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">10.1007/978-3-642-30793-5_13</a>.","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 &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , LNCS, vol. 7273, 203–218.","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. <a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">https://doi.org/10.1007/978-3-642-30793-5_13</a>."},"pubrep_id":"88","language":[{"iso":"eng"}],"oa":1,"date_created":"2018-12-11T12:01:43Z","volume":7273,"oa_version":"Submitted Version","title":"Synchronous interface theories and time triggered scheduling","day":"01","scopus_import":1,"author":[{"first_name":"Benoît","last_name":"Delahaye","full_name":"Delahaye, Benoît"},{"first_name":"Uli","last_name":"Fahrenberg","full_name":"Fahrenberg, Uli"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"file_date_updated":"2020-07-14T12:46:01Z","publication_status":"published","intvolume":"      7273","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."}],"has_accepted_license":"1","publist_id":"3539","year":"2012","date_published":"2012-06-01T00:00:00Z","acknowledgement":"Research partially supported by the Danish-Chinese Center for Cyber Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.","conference":{"location":"Stockholm, Sweden","name":"FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems ","end_date":"2012-06-16","start_date":"2012-06-13"},"status":"public","type":"conference","_id":"3155","date_updated":"2021-01-12T07:41:26Z","publisher":"Springer","alternative_title":["LNCS"],"doi":"10.1007/978-3-642-30793-5_13","quality_controlled":"1","ddc":["004"],"page":"203 - 218"},{"author":[{"first_name":"Eugene","last_name":"Asarin","full_name":"Asarin, Eugene"},{"full_name":"Donzé, Alexandre","last_name":"Donzé","first_name":"Alexandre"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"day":"01","scopus_import":1,"title":"Parametric identification of temporal properties","oa_version":"Submitted Version","volume":7186,"date_created":"2018-12-11T12:01:45Z","has_accepted_license":"1","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."}],"intvolume":"      7186","publication_status":"published","file_date_updated":"2020-07-14T12:46:01Z","month":"01","department":[{"_id":"ToHe"}],"file":[{"relation":"main_file","checksum":"ba4a75287008fc64b8fbf78a7476ec32","file_name":"2012_RV_Asarin.pdf","access_level":"open_access","content_type":"application/pdf","file_id":"7862","date_created":"2020-05-15T12:50:15Z","file_size":374726,"date_updated":"2020-07-14T12:46:01Z","creator":"dernst"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"ama":"Asarin E, Donzé A, Maler O, Nickovic D. Parametric identification of temporal properties. In: Vol 7186. Springer; 2012:147-160. doi:<a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">10.1007/978-3-642-29860-8_12</a>","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.","short":"E. Asarin, A. Donzé, O. Maler, D. Nickovic, in:, Springer, 2012, pp. 147–160.","chicago":"Asarin, Eugene, Alexandre Donzé, Oded Maler, and Dejan Nickovic. “Parametric Identification of Temporal Properties,” 7186:147–60. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">https://doi.org/10.1007/978-3-642-29860-8_12</a>.","ista":"Asarin E, Donzé A, Maler O, Nickovic D. 2012. Parametric identification of temporal properties. RV: Runtime Verification, LNCS, vol. 7186, 147–160.","apa":"Asarin, E., Donzé, A., Maler, O., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">https://doi.org/10.1007/978-3-642-29860-8_12</a>","mla":"Asarin, Eugene, et al. <i>Parametric Identification of Temporal Properties</i>. Vol. 7186, Springer, 2012, pp. 147–60, doi:<a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">10.1007/978-3-642-29860-8_12</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-642-29860-8_12","alternative_title":["LNCS"],"article_processing_charge":"No","publisher":"Springer","date_updated":"2021-01-12T07:41:29Z","_id":"3162","type":"conference","page":"147 - 160","ddc":["000"],"quality_controlled":"1","year":"2012","publist_id":"3525","status":"public","date_published":"2012-01-01T00:00:00Z","conference":{"start_date":"2011-09-27","end_date":"2011-09-30","name":"RV: Runtime Verification","location":"San Francisco, CA, United States"}},{"year":"2011","publist_id":"3253","status":"public","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"conference":{"location":"Aachen, Germany","name":"CONCUR: Concurrency Theory","start_date":"2011-09-06","end_date":"2011-09-09"},"date_published":"2011-01-01T00:00:00Z","alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-642-23217-6_27","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","_id":"3362","date_updated":"2021-01-12T07:42:57Z","type":"conference","page":"404 - 418","ddc":["000"],"quality_controlled":"1","month":"01","department":[{"_id":"ToHe"}],"file":[{"file_id":"7870","date_created":"2020-05-19T16:17:48Z","file_size":337125,"date_updated":"2020-07-14T12:46:10Z","creator":"dernst","relation":"main_file","checksum":"6bf2453d8e52e979ddb58d17325bad26","file_name":"2011_CONCUR_Fisher.pdf","content_type":"application/pdf","access_level":"open_access"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"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.","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.","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:<a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">10.1007/978-3-642-23217-6_27</a>","mla":"Fisher, Jasmin, et al. <i>Dynamic Reactive Modules</i>. Vol. 6901, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">10.1007/978-3-642-23217-6_27</a>.","apa":"Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">https://doi.org/10.1007/978-3-642-23217-6_27</a>","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.","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. <a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">https://doi.org/10.1007/978-3-642-23217-6_27</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","scopus_import":1,"author":[{"first_name":"Jasmin","last_name":"Fisher","full_name":"Fisher, Jasmin"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"},{"first_name":"Anmol","last_name":"Singh","full_name":"Singh, Anmol"},{"first_name":"Moshe","full_name":"Vardi, Moshe","last_name":"Vardi"}],"title":"Dynamic reactive modules","oa_version":"Submitted Version","volume":6901,"date_created":"2018-12-11T12:02:54Z","has_accepted_license":"1","intvolume":"      6901","abstract":[{"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.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:10Z","publication_status":"published"},{"project":[{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"status":"public","ec_funded":1,"date_published":"2010-09-08T00:00:00Z","conference":{"start_date":"2010-09-08","end_date":"2010-09-10","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Klosterneuburg, Austria"},"year":"2010","publist_id":"1090","page":"152 - 167","ddc":["004"],"quality_controlled":"1","doi":"10.1007/978-3-642-15297-9_13","alternative_title":["LNCS"],"editor":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A.","first_name":"Thomas A."},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"}],"publisher":"Springer","date_updated":"2021-01-12T07:56:27Z","_id":"4369","type":"conference","oa":1,"pubrep_id":"49","language":[{"iso":"eng"}],"citation":{"short":"D. Nickovic, N. Piterman, in:, T.A. Henzinger, K. Chatterjee (Eds.), Springer, 2010, pp. 152–167.","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.","ama":"Nickovic D, Piterman N. From MTL to deterministic timed automata. In: Henzinger TA, Chatterjee K, eds. Vol 6246. Springer; 2010:152-167. doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">10.1007/978-3-642-15297-9_13</a>","mla":"Nickovic, Dejan, and Nir Piterman. <i>From MTL to Deterministic Timed Automata</i>. Edited by Thomas A. Henzinger and Krishnendu Chatterjee, vol. 6246, Springer, 2010, pp. 152–67, doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">10.1007/978-3-642-15297-9_13</a>.","apa":"Nickovic, D., &#38; Piterman, N. (2010). From MTL to deterministic timed automata. In T. A. Henzinger &#38; K. Chatterjee (Eds.) (Vol. 6246, pp. 152–167). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">https://doi.org/10.1007/978-3-642-15297-9_13</a>","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. <a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">https://doi.org/10.1007/978-3-642-15297-9_13</a>.","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."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","month":"09","department":[{"_id":"ToHe"}],"file":[{"date_created":"2018-12-12T10:13:43Z","file_size":249789,"creator":"system","date_updated":"2020-07-14T12:46:27Z","file_id":"5028","file_name":"IST-2012-49-v1+1_From_MTL_to_deterministic_timed_automata.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"b0ca5f5fbe8a3d20ccbc6f51a344a459"}],"has_accepted_license":"1","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."}],"intvolume":"      6246","publication_status":"published","file_date_updated":"2020-07-14T12:46:27Z","author":[{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"}],"day":"08","scopus_import":1,"oa_version":"Submitted Version","title":"From MTL to deterministic timed automata","volume":6246,"date_created":"2018-12-11T12:08:30Z"},{"publist_id":"1080","month":"06","year":"2010","date_published":"2010-06-01T00:00:00Z","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.","issue":"2","citation":{"ama":"Jones K, Konrad V, Nickovic D. Analog property checkers: a DDR2 case study. <i>Formal Methods in System Design</i>. 2010;36(2):114-130. doi:<a href=\"https://doi.org/10.1007/s10703-009-0085-x\">10.1007/s10703-009-0085-x</a>","ieee":"K. Jones, V. Konrad, and D. Nickovic, “Analog property checkers: a DDR2 case study,” <i>Formal Methods in System Design</i>, vol. 36, no. 2. Springer, pp. 114–130, 2010.","short":"K. Jones, V. Konrad, D. Nickovic, Formal Methods in System Design 36 (2010) 114–130.","ista":"Jones K, Konrad V, Nickovic D. 2010. Analog property checkers: a DDR2 case study. Formal Methods in System Design. 36(2), 114–130.","chicago":"Jones, Kevin, Victor Konrad, and Dejan Nickovic. “Analog Property Checkers: A DDR2 Case Study.” <i>Formal Methods in System Design</i>. Springer, 2010. <a href=\"https://doi.org/10.1007/s10703-009-0085-x\">https://doi.org/10.1007/s10703-009-0085-x</a>.","apa":"Jones, K., Konrad, V., &#38; Nickovic, D. (2010). Analog property checkers: a DDR2 case study. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-009-0085-x\">https://doi.org/10.1007/s10703-009-0085-x</a>","mla":"Jones, Kevin, et al. “Analog Property Checkers: A DDR2 Case Study.” <i>Formal Methods in System Design</i>, vol. 36, no. 2, Springer, 2010, pp. 114–30, doi:<a href=\"https://doi.org/10.1007/s10703-009-0085-x\">10.1007/s10703-009-0085-x</a>."},"publication":"Formal Methods in System Design","status":"public","extern":1,"oa":1,"type":"journal_article","date_created":"2018-12-11T12:08:33Z","date_updated":"2021-01-12T07:56:31Z","volume":36,"_id":"4379","title":"Analog property checkers: a DDR2 case study","publisher":"Springer","doi":"10.1007/s10703-009-0085-x","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","last_name":"Nickovic","full_name":"Dejan Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"day":"01","quality_controlled":0,"publication_status":"published","main_file_link":[{"open_access":"1","url":"http://openaccess.city.ac.uk/1066/"}],"abstract":[{"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.\n\nIn 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.\n","lang":"eng"}],"intvolume":"        36","page":"114 - 130"},{"type":"conference","_id":"4389","date_updated":"2021-01-12T07:56:36Z","publisher":"IEEE","doi":"10.1109/ACSD.2010.26","quality_controlled":"1","ddc":["004"],"page":"77 - 84","publist_id":"1069","year":"2010","conference":{"name":"ACSD: Application of Concurrency to System Design"},"date_published":"2010-08-23T00:00:00Z","status":"public","date_created":"2018-12-11T12:08:36Z","oa_version":"Submitted Version","title":"Robustness of sequential circuits","scopus_import":1,"day":"23","author":[{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Legay","full_name":"Legay, Axel","first_name":"Axel"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"}],"file_date_updated":"2020-07-14T12:46:28Z","publication_status":"published","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","file":[{"date_created":"2018-12-12T10:09:10Z","file_size":159920,"date_updated":"2020-07-14T12:46:28Z","creator":"system","file_id":"4733","file_name":"IST-2012-44-v1+1_Robustness_of_sequential_circuits.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"42b2952bfc6b6974617bd554842b904a"}],"department":[{"_id":"ToHe"}],"month":"08","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Doyen L, Henzinger TA, Legay A, Nickovic D. Robustness of sequential circuits. In: IEEE; 2010:77-84. doi:<a href=\"https://doi.org/10.1109/ACSD.2010.26\">10.1109/ACSD.2010.26</a>","short":"L. Doyen, T.A. Henzinger, A. Legay, D. Nickovic, in:, IEEE, 2010, pp. 77–84.","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.","chicago":"Doyen, Laurent, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Robustness of Sequential Circuits,” 77–84. IEEE, 2010. <a href=\"https://doi.org/10.1109/ACSD.2010.26\">https://doi.org/10.1109/ACSD.2010.26</a>.","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. <i>Robustness of Sequential Circuits</i>. IEEE, 2010, pp. 77–84, doi:<a href=\"https://doi.org/10.1109/ACSD.2010.26\">10.1109/ACSD.2010.26</a>.","apa":"Doyen, L., Henzinger, T. A., Legay, A., &#38; Nickovic, D. (2010). Robustness of sequential circuits (pp. 77–84). Presented at the ACSD: Application of Concurrency to System Design, IEEE. <a href=\"https://doi.org/10.1109/ACSD.2010.26\">https://doi.org/10.1109/ACSD.2010.26</a>"},"pubrep_id":"44","language":[{"iso":"eng"}],"oa":1},{"date_updated":"2023-02-14T10:42:38Z","_id":"4371","type":"book_chapter","date_created":"2018-12-11T12:08:30Z","author":[{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli, Amir"}],"doi":"10.1007/978-3-540-78127-1_26","day":"11","alternative_title":["LNCS"],"scopus_import":"1","article_processing_charge":"No","title":"Checking Temporal Properties of Discrete, Timed and Continuous Behaviors","oa_version":"None","publisher":"Springer","publication_identifier":{"isbn":["9783540781264"]},"publication_status":"published","quality_controlled":"1","page":"475 - 505","abstract":[{"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.","lang":"eng"}],"publist_id":"1087","year":"2008","month":"03","citation":{"ieee":"O. Maler, D. Nickovic, and A. Pnueli, “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors,” in <i>Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, Springer, 2008, pp. 475–505.","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.","ama":"Maler O, Nickovic D, Pnueli A. Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>. Springer; 2008:475-505. doi:<a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">10.1007/978-3-540-78127-1_26</a>","apa":"Maler, O., Nickovic, D., &#38; Pnueli, A. (2008). Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In <i>Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i> (pp. 475–505). Springer. <a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">https://doi.org/10.1007/978-3-540-78127-1_26</a>","mla":"Maler, Oded, et al. “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.” <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, Springer, 2008, pp. 475–505, doi:<a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">10.1007/978-3-540-78127-1_26</a>.","chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.” In <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, 475–505. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">https://doi.org/10.1007/978-3-540-78127-1_26</a>.","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."},"date_published":"2008-03-11T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","publication":"Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday","status":"public","language":[{"iso":"eng"}]},{"month":"09","year":"2007","publist_id":"1089","status":"public","extern":1,"conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"date_published":"2007-09-20T00:00:00Z","citation":{"mla":"Nickovic, Dejan, and Oded Maler. <i>AMT: A Property-Based Monitoring Tool for Analog Systems</i>. Springer, 2007, pp. 304–19, doi:<a href=\"https://doi.org/1567\">1567</a>.","apa":"Nickovic, D., &#38; 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. <a href=\"https://doi.org/1567\">https://doi.org/1567</a>","chicago":"Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool for Analog Systems,” 304–19. Springer, 2007. <a href=\"https://doi.org/1567\">https://doi.org/1567</a>.","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.","short":"D. Nickovic, O. Maler, in:, Springer, 2007, pp. 304–319.","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.","ama":"Nickovic D, Maler O. AMT: a property-based monitoring tool for analog systems. In: Springer; 2007:304-319. doi:<a href=\"https://doi.org/1567\">1567</a>"},"publisher":"Springer","title":"AMT: a property-based monitoring tool for analog systems","day":"20","alternative_title":["LNCS"],"author":[{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Dejan Nickovic","first_name":"Dejan"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"}],"doi":"1567","date_created":"2018-12-11T12:08:30Z","type":"conference","_id":"4368","date_updated":"2021-01-12T07:56:27Z","page":"304 - 319","quality_controlled":0,"publication_status":"published"},{"citation":{"chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers from Bounded-Response Properties,” 95–107. Springer, 2007. <a href=\"https://doi.org/1568\">https://doi.org/1568</a>.","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.","apa":"Maler, O., Nickovic, D., &#38; Pnueli, A. (2007). On synthesizing controllers from bounded-response properties (pp. 95–107). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1568\">https://doi.org/1568</a>","mla":"Maler, Oded, et al. <i>On Synthesizing Controllers from Bounded-Response Properties</i>. Springer, 2007, pp. 95–107, doi:<a href=\"https://doi.org/1568\">1568</a>.","ama":"Maler O, Nickovic D, Pnueli A. On synthesizing controllers from bounded-response properties. In: Springer; 2007:95-107. doi:<a href=\"https://doi.org/1568\">1568</a>","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.","short":"O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2007, pp. 95–107."},"date_published":"2007-01-01T00:00:00Z","conference":{"name":"CAV: Computer Aided Verification"},"status":"public","extern":1,"publist_id":"1086","year":"2007","month":"01","quality_controlled":0,"publication_status":"published","page":"95 - 107","_id":"4370","date_updated":"2021-01-12T07:56:28Z","date_created":"2018-12-11T12:08:30Z","type":"conference","alternative_title":["Lecture Notes in Computer Science"],"day":"01","doi":"1568","author":[{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Dejan","full_name":"Dejan Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli,Amir"}],"publisher":"Springer","title":"On synthesizing controllers from bounded-response properties"},{"publist_id":"1084","year":"2006","month":"01","citation":{"short":"O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 2–16.","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.","ama":"Maler O, Nickovic D, Pnueli A. Real Time Temporal Logic: Past, Present, Future. In: Springer; 2006:2-16. doi:<a href=\"https://doi.org/1571\">1571</a>","mla":"Maler, Oded, et al. <i>Real Time Temporal Logic: Past, Present, Future</i>. Springer, 2006, pp. 2–16, doi:<a href=\"https://doi.org/1571\">1571</a>.","apa":"Maler, O., Nickovic, D., &#38; 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. <a href=\"https://doi.org/1571\">https://doi.org/1571</a>","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.","chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Real Time Temporal Logic: Past, Present, Future,” 2–16. Springer, 2006. <a href=\"https://doi.org/1571\">https://doi.org/1571</a>."},"date_published":"2006-01-23T00:00:00Z","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"status":"public","extern":1,"_id":"4373","date_updated":"2021-01-12T07:56:29Z","date_created":"2018-12-11T12:08:31Z","type":"conference","day":"23","alternative_title":["LNCS"],"doi":"1571","author":[{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Dejan Nickovic","last_name":"Nickovic","first_name":"Dejan"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli,Amir"}],"title":"Real Time Temporal Logic: Past, Present, Future","publisher":"Springer","quality_controlled":0,"publication_status":"published","page":"2 - 16"},{"quality_controlled":0,"publication_status":"published","page":"274 - 289","_id":"4374","date_updated":"2021-01-12T07:56:30Z","date_created":"2018-12-11T12:08:31Z","type":"conference","alternative_title":["LNCS"],"day":"19","doi":"1570","author":[{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Dejan","full_name":"Dejan Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli,Amir"}],"publisher":"Springer","title":"From MITL to Timed Automata","citation":{"chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “From MITL to Timed Automata,” 274–89. Springer, 2006. <a href=\"https://doi.org/1570\">https://doi.org/1570</a>.","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. <i>From MITL to Timed Automata</i>. Springer, 2006, pp. 274–89, doi:<a href=\"https://doi.org/1570\">1570</a>.","apa":"Maler, O., Nickovic, D., &#38; Pnueli, A. (2006). From MITL to Timed Automata (pp. 274–289). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. <a href=\"https://doi.org/1570\">https://doi.org/1570</a>","ama":"Maler O, Nickovic D, Pnueli A. From MITL to Timed Automata. In: Springer; 2006:274-289. doi:<a href=\"https://doi.org/1570\">1570</a>","short":"O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 274–289.","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."},"date_published":"2006-10-19T00:00:00Z","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"extern":1,"status":"public","publist_id":"1085","year":"2006","month":"10"}]