[{"month":"08","publication_identifier":{"eissn":["1611-3349"],"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"]},"conference":{"end_date":"2019-08-29","start_date":"2019-08-27","location":"Amsterdam, The Netherlands","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"doi":"10.1007/978-3-030-29662-9_8","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11514"}],"oa":1,"external_id":{"isi":["000611677700008"],"arxiv":["1907.11514"]},"isi":1,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"author":[{"full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"date_created":"2020-01-05T23:00:47Z","date_updated":"2023-09-06T14:55:15Z","volume":11750,"year":"2019","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","day":"13","article_processing_charge":"No","scopus_import":"1","date_published":"2019-08-13T00:00:00Z","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","citation":{"chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In 17th International Conference on Formal Modeling and Analysis of Timed Systems, 11750:123–41. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_8.","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.","mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” 17th International Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:10.1007/978-3-030-29662-9_8.","apa":"Kong, H., Bartocci, E., Jiang, Y., & Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In 17th International Conference on Formal Modeling and Analysis of Timed Systems (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_8","ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in 17th International Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141.","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: 17th International Conference on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature; 2019:123-141. doi:10.1007/978-3-030-29662-9_8"},"page":"123-141","abstract":[{"lang":"eng","text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","_id":"7231","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","status":"public","intvolume":" 11750"},{"month":"07","external_id":{"isi":["000491481600024"]},"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","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"quality_controlled":"1","isi":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"CAV: Computer Aided Verification","end_date":"2018-07-17","location":"Oxford, United Kingdom","start_date":"2018-07-14"},"doi":"10.1007/978-3-319-96145-3_24","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:53Z","publist_id":"7781","license":"https://creativecommons.org/licenses/by/4.0/","year":"2018","acknowledgement":"Austrian Science Fund FWF: S11402-N23, S11405-N23, Z211-N32","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","author":[{"full_name":"Kong, Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","first_name":"Hui","last_name":"Kong"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"date_updated":"2023-09-15T12:12:08Z","date_created":"2018-12-11T11:44:51Z","volume":10981,"scopus_import":"1","day":"18","has_accepted_license":"1","article_processing_charge":"No","citation":{"chicago":"Kong, Hui, Ezio Bartocci, and Thomas A Henzinger. “Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes,” 10981:449–67. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_24.","short":"H. Kong, E. Bartocci, T.A. Henzinger, in:, Springer, 2018, pp. 449–467.","mla":"Kong, Hui, et al. Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. Vol. 10981, Springer, 2018, pp. 449–67, doi:10.1007/978-3-319-96145-3_24.","ieee":"H. Kong, E. Bartocci, and T. A. Henzinger, “Reachable set over-approximation for nonlinear systems using piecewise barrier tubes,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981, pp. 449–467.","apa":"Kong, H., Bartocci, E., & Henzinger, T. A. (2018). Reachable set over-approximation for nonlinear systems using piecewise barrier tubes (Vol. 10981, pp. 449–467). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96145-3_24","ista":"Kong H, Bartocci E, Henzinger TA. 2018. Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. CAV: Computer Aided Verification, LNCS, vol. 10981, 449–467.","ama":"Kong H, Bartocci E, Henzinger TA. Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. In: Vol 10981. Springer; 2018:449-467. doi:10.1007/978-3-319-96145-3_24"},"page":"449 - 467","date_published":"2018-07-18T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We address the problem of analyzing the reachable set of a polynomial nonlinear continuous system by over-approximating the flowpipe of its dynamics. The common approach to tackle this problem is to perform a numerical integration over a given time horizon based on Taylor expansion and interval arithmetic. However, this method results to be very conservative when there is a large difference in speed between trajectories as time progresses. In this paper, we propose to use combinations of barrier functions, which we call piecewise barrier tube (PBT), to over-approximate flowpipe. The basic idea of PBT is that for each segment of a flowpipe, a coarse box which is big enough to contain the segment is constructed using sampled simulation and then in the box we compute by linear programming a set of barrier functions (called barrier tube or BT for short) which work together to form a tube surrounding the flowpipe. The benefit of using PBT is that (1) BT is independent of time and hence can avoid being stretched and deformed by time; and (2) a small number of BTs can form a tight over-approximation for the flowpipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype called PBTS in C++. Experiments on some benchmark systems show that our approach is effective."}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"142","status":"public","title":"Reachable set over-approximation for nonlinear systems using piecewise barrier tubes","ddc":["000"],"intvolume":" 10981","file":[{"file_id":"5718","relation":"main_file","date_created":"2018-12-17T15:57:06Z","date_updated":"2020-07-14T12:44:53Z","checksum":"fd95e8026deacef3dc752a733bb9355f","file_name":"2018_LNCS_Kong.pdf","access_level":"open_access","creator":"dernst","file_size":5591566,"content_type":"application/pdf"}],"oa_version":"Published Version"},{"scopus_import":"1","article_processing_charge":"No","day":"01","citation":{"ista":"Jiang Y, Liu H, Song H, Kong H, Wang R, Guan Y, Sha L. 2018. Safety-assured model-driven design of the multifunction vehicle bus controller. IEEE Transactions on Intelligent Transportation Systems. 19(10), 3320–3333.","ieee":"Y. Jiang et al., “Safety-assured model-driven design of the multifunction vehicle bus controller,” IEEE Transactions on Intelligent Transportation Systems, vol. 19, no. 10. IEEE, pp. 3320–3333, 2018.","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Wang, R., Guan, Y., & Sha, L. (2018). Safety-assured model-driven design of the multifunction vehicle bus controller. IEEE Transactions on Intelligent Transportation Systems. IEEE. https://doi.org/10.1109/TITS.2017.2778077","ama":"Jiang Y, Liu H, Song H, et al. Safety-assured model-driven design of the multifunction vehicle bus controller. IEEE Transactions on Intelligent Transportation Systems. 2018;19(10):3320-3333. doi:10.1109/TITS.2017.2778077","chicago":"Jiang, Yu, Han Liu, Huobing Song, Hui Kong, Rui Wang, Yong Guan, and Lui Sha. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” IEEE Transactions on Intelligent Transportation Systems. IEEE, 2018. https://doi.org/10.1109/TITS.2017.2778077.","mla":"Jiang, Yu, et al. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” IEEE Transactions on Intelligent Transportation Systems, vol. 19, no. 10, IEEE, 2018, pp. 3320–33, doi:10.1109/TITS.2017.2778077.","short":"Y. Jiang, H. Liu, H. Song, H. Kong, R. Wang, Y. Guan, L. Sha, IEEE Transactions on Intelligent Transportation Systems 19 (2018) 3320–3333."},"publication":"IEEE Transactions on Intelligent Transportation Systems","page":"3320 - 3333","date_published":"2018-01-01T00:00:00Z","type":"journal_article","issue":"10","abstract":[{"text":"In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.","lang":"eng"}],"_id":"434","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","intvolume":" 19","title":"Safety-assured model-driven design of the multifunction vehicle bus controller","status":"public","oa_version":"None","month":"01","external_id":{"isi":["000446651100020"]},"isi":1,"quality_controlled":"1","doi":"10.1109/TITS.2017.2778077","language":[{"iso":"eng"}],"publist_id":"7389","year":"2018","publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1205"}]},"author":[{"full_name":"Jiang, Yu","last_name":"Jiang","first_name":"Yu"},{"full_name":"Liu, Han","last_name":"Liu","first_name":"Han"},{"full_name":"Song, Huobing","last_name":"Song","first_name":"Huobing"},{"full_name":"Kong, Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","first_name":"Hui","last_name":"Kong"},{"first_name":"Rui","last_name":"Wang","full_name":"Wang, Rui"},{"last_name":"Guan","first_name":"Yong","full_name":"Guan, Yong"},{"full_name":"Sha, Lui","first_name":"Lui","last_name":"Sha"}],"volume":19,"date_updated":"2023-09-18T08:12:49Z","date_created":"2018-12-11T11:46:27Z"},{"date_created":"2018-12-11T11:47:47Z","date_updated":"2021-01-12T08:08:17Z","author":[{"full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","first_name":"Hui"},{"first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"publisher":"ACM","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2017","publist_id":"7067","file_date_updated":"2020-07-14T12:47:34Z","language":[{"iso":"eng"}],"doi":"10.1145/3049797.3049814","conference":{"end_date":"2017-04-20","location":"Pittsburgh, PA, United States","start_date":"2017-04-18","name":"HSCC: Hybrid Systems Computation and Control "},"quality_controlled":"1","oa":1,"publication_identifier":{"isbn":["978-145034590-3"]},"month":"04","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2017-817-v1+1_p163-kong.pdf","content_type":"application/pdf","file_size":1650530,"creator":"system","relation":"main_file","file_id":"4873","checksum":"b7667434cbf5b5f0ade3bea1dbe5bf63","date_updated":"2020-07-14T12:47:34Z","date_created":"2018-12-12T10:11:20Z"}],"pubrep_id":"817","ddc":["000"],"title":"Safety verification of nonlinear hybrid systems based on invariant clusters","status":"public","_id":"663","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u→, x→) = 0, parametric in u→, which can yield an infinite number of concrete invariants by assigning different values to u→ so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial right-hand sides, given a template multivariate polynomial g(u→, x→), an invariant cluster can be obtained by first computing the remainder of the Lie derivative of g(u→, x→) divided by g(u→, x→) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is efficient. ","lang":"eng"}],"type":"conference","date_published":"2017-04-01T00:00:00Z","page":"163 - 172","citation":{"short":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, T.A. Henzinger, in:, Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–172.","mla":"Kong, Hui, et al. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–72, doi:10.1145/3049797.3049814.","chicago":"Kong, Hui, Sergiy Bogomolov, Christian Schilling, Yu Jiang, and Thomas A Henzinger. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” In Proceedings of the 20th International Conference on Hybrid Systems, 163–72. ACM, 2017. https://doi.org/10.1145/3049797.3049814.","ama":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. Safety verification of nonlinear hybrid systems based on invariant clusters. In: Proceedings of the 20th International Conference on Hybrid Systems. ACM; 2017:163-172. doi:10.1145/3049797.3049814","ieee":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, and T. A. Henzinger, “Safety verification of nonlinear hybrid systems based on invariant clusters,” in Proceedings of the 20th International Conference on Hybrid Systems, Pittsburgh, PA, United States, 2017, pp. 163–172.","apa":"Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., & Henzinger, T. A. (2017). Safety verification of nonlinear hybrid systems based on invariant clusters. In Proceedings of the 20th International Conference on Hybrid Systems (pp. 163–172). Pittsburgh, PA, United States: ACM. https://doi.org/10.1145/3049797.3049814","ista":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. 2017. Safety verification of nonlinear hybrid systems based on invariant clusters. Proceedings of the 20th International Conference on Hybrid Systems. HSCC: Hybrid Systems Computation and Control , 163–172."},"publication":"Proceedings of the 20th International Conference on Hybrid Systems","has_accepted_license":"1","day":"01","scopus_import":1},{"date_published":"2017-09-01T00:00:00Z","citation":{"ama":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7","ista":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 116–132.","apa":"Bogomolov, S., Giacobbe, M., Henzinger, T. A., & Kong, H. (2017). Conic abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_7","ieee":"S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.","mla":"Bogomolov, Sergiy, et al. Conic Abstractions for Hybrid Systems. Vol. 10419, Springer, 2017, pp. 116–32, doi:10.1007/978-3-319-65765-3_7.","short":"S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.","chicago":"Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_7."},"page":"116 - 132","has_accepted_license":"1","day":"01","scopus_import":1,"pubrep_id":"831","oa_version":"Submitted Version","file":[{"date_updated":"2020-07-14T12:47:31Z","date_created":"2018-12-12T10:12:38Z","checksum":"faf546914ba29bcf9974ee36b6b16750","relation":"main_file","file_id":"4956","content_type":"application/pdf","file_size":3806864,"creator":"system","file_name":"IST-2017-831-v1+1_main.pdf","access_level":"open_access"}],"_id":"647","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["005"],"status":"public","title":"Conic abstractions for hybrid systems","abstract":[{"lang":"eng","text":"Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems."}],"type":"conference","alternative_title":["LNCS"],"doi":"10.1007/978-3-319-65765-3_7","conference":{"location":"Berlin, Germany","start_date":"2017-09-05","end_date":"2017-09-07","name":"FORMATS: Formal Modelling and Analysis of Timed Systems"},"language":[{"iso":"eng"}],"oa":1,"project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","publication_identifier":{"isbn":["978-331965764-6"]},"month":"09","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"6894"}]},"author":[{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","first_name":"Mirco","last_name":"Giacobbe","full_name":"Giacobbe, Mirco"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","first_name":"Hui","last_name":"Kong","full_name":"Kong, Hui"}],"volume":"10419 ","date_updated":"2023-09-07T12:53:00Z","date_created":"2018-12-11T11:47:41Z","year":"2017","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","publist_id":"7129","file_date_updated":"2020-07-14T12:47:31Z"},{"date_published":"2016-09-25T00:00:00Z","page":"128 - 144","citation":{"short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.","mla":"Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol. 9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.","chicago":"Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger, Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,” 9957:128–44. Springer, 2016. https://doi.org/10.1007/978-3-319-47151-8_9.","ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9","ieee":"H. Kong et al., “Discrete abstraction of multiaffine systems,” presented at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.","apa":"Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. https://doi.org/10.1007/978-3-319-47151-8_9","ista":"Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology, LNCS, vol. 9957, 128–144."},"has_accepted_license":"1","day":"25","scopus_import":1,"file":[{"checksum":"994e164b558c47bacf8dc066dd27c8fc","date_updated":"2020-07-14T12:44:39Z","date_created":"2018-12-12T10:10:49Z","relation":"main_file","file_id":"4840","content_type":"application/pdf","file_size":683955,"creator":"system","access_level":"open_access","file_name":"IST-2017-781-v1+1_main.pdf"}],"oa_version":"Submitted Version","pubrep_id":"781","intvolume":" 9957","status":"public","ddc":["005"],"title":"Discrete abstraction of multiaffine systems","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1227","abstract":[{"text":"Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-47151-8_9","conference":{"end_date":"2016-10-21","location":"Grenoble, France","start_date":"2016-10-20","name":"HSB: Hybrid Systems Biology"},"project":[{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","oa":1,"month":"09","volume":9957,"date_updated":"2021-01-12T06:49:13Z","date_created":"2018-12-11T11:50:49Z","author":[{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","first_name":"Christian"}],"publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2016","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","publist_id":"6107","file_date_updated":"2020-07-14T12:44:39Z"},{"language":[{"iso":"eng"}],"doi":"10.1109/RTAS.2016.7461337","conference":{"end_date":"2016-04-14","location":"Vienna, Austria","start_date":"2016-04-11","name":"RTAS: Real-time and Embedded Technology and Applications Symposium"},"quality_controlled":"1","oa":1,"month":"04","date_created":"2018-12-11T11:50:58Z","date_updated":"2021-01-12T06:49:26Z","author":[{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"first_name":"Yixiao","last_name":"Yang","full_name":"Yang, Yixiao"},{"full_name":"Liu, Han","last_name":"Liu","first_name":"Han"},{"full_name":"Kong, Hui","last_name":"Kong","first_name":"Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gu, Ming","first_name":"Ming","last_name":"Gu"},{"last_name":"Sun","first_name":"Jiaguang","full_name":"Sun, Jiaguang"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2016","acknowledgement":"This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.","publist_id":"6069","file_date_updated":"2020-07-14T12:44:41Z","article_number":"7461337","date_published":"2016-04-27T00:00:00Z","citation":{"ieee":"Y. Jiang et al., “From stateflow simulation to verified implementation: A verification approach and a real-time train controller design,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria, 2016.","apa":"Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016). From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. https://doi.org/10.1109/RTAS.2016.7461337","ista":"Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. RTAS: Real-time and Embedded Technology and Applications Symposium, 7461337.","ama":"Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. In: IEEE; 2016. doi:10.1109/RTAS.2016.7461337","chicago":"Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design.” IEEE, 2016. https://doi.org/10.1109/RTAS.2016.7461337.","short":"Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.","mla":"Jiang, Yu, et al. From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design. 7461337, IEEE, 2016, doi:10.1109/RTAS.2016.7461337."},"has_accepted_license":"1","day":"27","scopus_import":1,"file":[{"file_name":"IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf","access_level":"open_access","creator":"system","file_size":1293599,"content_type":"application/pdf","file_id":"4949","relation":"main_file","date_updated":"2020-07-14T12:44:41Z","date_created":"2018-12-12T10:12:31Z","checksum":"42f0462911cc9957f2356b12fb33b4b6"}],"oa_version":"Submitted Version","pubrep_id":"780","ddc":["005"],"status":"public","title":"From stateflow simulation to verified implementation: A verification approach and a real-time train controller design","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1256","abstract":[{"lang":"eng","text":"Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform."}],"type":"conference"},{"year":"2016","_id":"479","acknowledgement":"This work is supported by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, and NSFC 61303014.\r\nThe authors thank Dr. Bobby and Dr. Hill at Carle Hospital, Urbana, IL for their help with the discussion on medical knowledge.\r\n\r\n","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","title":"Use runtime verification to improve the quality of medical care practice","department":[{"_id":"ToHe"}],"publisher":"IEEE","author":[{"full_name":"Jiang, Yu","last_name":"Jiang","first_name":"Yu"},{"first_name":"Han","last_name":"Liu","full_name":"Liu, Han"},{"last_name":"Kong","first_name":"Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui"},{"full_name":"Wang, Rui","last_name":"Wang","first_name":"Rui"},{"full_name":"Hosseini, Mohamad","first_name":"Mohamad","last_name":"Hosseini"},{"last_name":"Sun","first_name":"Jiaguang","full_name":"Sun, Jiaguang"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"date_created":"2018-12-11T11:46:42Z","date_updated":"2021-01-12T08:00:55Z","oa_version":"None","type":"conference","alternative_title":["Proceedings International Conference on Software Engineering"],"abstract":[{"lang":"eng","text":"Clinical guidelines and decision support systems (DSS) play an important role in daily practices of medicine. Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care. During the collaboration with Carle hospital to develop a DSS, we identify that, for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties in guidelines, which brings new challenges to current simulation based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios, and applied the proposed technique to assist existing DSS. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital"}],"publist_id":"7341","publication":"Proceedings of the 38th International Conference on Software Engineering Companion ","citation":{"chicago":"Jiang, Yu, Han Liu, Hui Kong, Rui Wang, Mohamad Hosseini, Jiaguang Sun, and Lui Sha. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” In Proceedings of the 38th International Conference on Software Engineering Companion , 112–21. IEEE, 2016. https://doi.org/10.1145/2889160.2889233.","mla":"Jiang, Yu, et al. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” Proceedings of the 38th International Conference on Software Engineering Companion , IEEE, 2016, pp. 112–21, doi:10.1145/2889160.2889233.","short":"Y. Jiang, H. Liu, H. Kong, R. Wang, M. Hosseini, J. Sun, L. Sha, in:, Proceedings of the 38th International Conference on Software Engineering Companion , IEEE, 2016, pp. 112–121.","ista":"Jiang Y, Liu H, Kong H, Wang R, Hosseini M, Sun J, Sha L. 2016. Use runtime verification to improve the quality of medical care practice. Proceedings of the 38th International Conference on Software Engineering Companion . ICSE: International Conference on Software Engineering, Proceedings International Conference on Software Engineering, , 112–121.","apa":"Jiang, Y., Liu, H., Kong, H., Wang, R., Hosseini, M., Sun, J., & Sha, L. (2016). Use runtime verification to improve the quality of medical care practice. In Proceedings of the 38th International Conference on Software Engineering Companion (pp. 112–121). Austin, TX, USA: IEEE. https://doi.org/10.1145/2889160.2889233","ieee":"Y. Jiang et al., “Use runtime verification to improve the quality of medical care practice,” in Proceedings of the 38th International Conference on Software Engineering Companion , Austin, TX, USA, 2016, pp. 112–121.","ama":"Jiang Y, Liu H, Kong H, et al. Use runtime verification to improve the quality of medical care practice. In: Proceedings of the 38th International Conference on Software Engineering Companion . IEEE; 2016:112-121. doi:10.1145/2889160.2889233"},"quality_controlled":"1","page":"112 - 121","conference":{"name":"ICSE: International Conference on Software Engineering","start_date":"2016-05-14","location":"Austin, TX, USA","end_date":"2016-05-22"},"doi":"10.1145/2889160.2889233","date_published":"2016-05-14T00:00:00Z","language":[{"iso":"eng"}],"scopus_import":1,"day":"14","month":"05"},{"date_created":"2018-12-11T11:50:42Z","date_updated":"2023-09-18T08:12:48Z","volume":9995,"author":[{"full_name":"Jiang, Yu","first_name":"Yu","last_name":"Jiang"},{"first_name":"Han","last_name":"Liu","full_name":"Liu, Han"},{"last_name":"Song","first_name":"Houbing","full_name":"Song, Houbing"},{"full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941"},{"last_name":"Gu","first_name":"Ming","full_name":"Gu, Ming"},{"last_name":"Sun","first_name":"Jiaguang","full_name":"Sun, Jiaguang"},{"full_name":"Sha, Lui","first_name":"Lui","last_name":"Sha"}],"related_material":{"record":[{"id":"434","status":"public","relation":"later_version"}]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","acknowledgement":"This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies) of China, and the National Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23.\r\n","year":"2016","file_date_updated":"2020-07-14T12:44:39Z","publist_id":"6144","language":[{"iso":"eng"}],"conference":{"location":"Limassol, Cyprus","start_date":"2016-11-09","end_date":"2016-11-11","name":"FM: International Symposium on Formal Methods"},"doi":"10.1007/978-3-319-48989-6_47","quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"oa":1,"month":"11","oa_version":"Submitted Version","file":[{"file_id":"4673","relation":"main_file","date_created":"2018-12-12T10:08:13Z","date_updated":"2020-07-14T12:44:39Z","checksum":"fea0b3fae9a2a42e8bfec59840e30d8c","file_name":"IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":281501}],"pubrep_id":"783","status":"public","title":"Safety assured formal model driven design of the multifunction vehicle bus controller","ddc":["004"],"intvolume":" 9995","_id":"1205","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network."}],"alternative_title":["LNCS"],"type":"conference","date_published":"2016-11-08T00:00:00Z","page":"757 - 763","citation":{"ama":"Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:10.1007/978-3-319-48989-6_47","ista":"Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured formal model driven design of the multifunction vehicle bus controller. FM: International Symposium on Formal Methods, LNCS, vol. 9995, 757–763.","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus: Springer. https://doi.org/10.1007/978-3-319-48989-6_47","ieee":"Y. Jiang et al., “Safety assured formal model driven design of the multifunction vehicle bus controller,” presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.","mla":"Jiang, Yu, et al. Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller. Vol. 9995, Springer, 2016, pp. 757–63, doi:10.1007/978-3-319-48989-6_47.","short":"Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer, 2016, pp. 757–763.","chicago":"Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller,” 9995:757–63. Springer, 2016. https://doi.org/10.1007/978-3-319-48989-6_47."},"day":"08","has_accepted_license":"1","scopus_import":1},{"scopus_import":1,"day":"28","has_accepted_license":"1","article_processing_charge":"No","citation":{"short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","mla":"Bogomolov, Sergiy, et al. Abstraction-Based Parameter Synthesis for Multiaffine Systems. Vol. 9434, Springer, 2015, pp. 19–35, doi:10.1007/978-3-319-26287-1_2.","chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_2.","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:10.1007/978-3-319-26287-1_2","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., & Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_2","ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35."},"page":"19 - 35","date_published":"2015-11-28T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1605","status":"public","title":"Abstraction-based parameter synthesis for multiaffine systems","ddc":["000"],"intvolume":" 9434","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"2015_LNCS_Bogomolov.pdf","content_type":"application/pdf","file_size":1053207,"creator":"dernst","relation":"main_file","file_id":"7851","checksum":"3aab260f3f34641d622030ba22645b3e","date_updated":"2020-07-14T12:45:05Z","date_created":"2020-05-15T08:43:19Z"}],"month":"11","oa":1,"quality_controlled":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"conference":{"location":"Haifa, Israel","start_date":"2015-11-17","end_date":"2015-11-19","name":"HVC: Haifa Verification Conference"},"doi":"10.1007/978-3-319-26287-1_2","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:45:05Z","ec_funded":1,"publist_id":"5561","acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","year":"2015","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","author":[{"first_name":"Sergiy","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy"},{"first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"full_name":"Batt, Grégory","first_name":"Grégory","last_name":"Batt"},{"first_name":"Hui","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","full_name":"Kong, Hui"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"}],"date_created":"2018-12-11T11:52:59Z","date_updated":"2021-01-12T06:51:56Z","volume":9434}]