---
_id: '7231'
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.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
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'
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'
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.
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.'
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.
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.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:47Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2023-09-06T14:55:15Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_8
external_id:
arxiv:
- '1907.11514'
isi:
- '000611677700008'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1907.11514
month: '08'
oa: 1
oa_version: Preprint
page: 123-141
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 17th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9661-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...
---
_id: '142'
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.
acknowledgement: 'Austrian Science Fund FWF: S11402-N23, S11405-N23, Z211-N32'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
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'
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'
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.
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.'
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.'
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.
short: H. Kong, E. Bartocci, T.A. Henzinger, in:, Springer, 2018, pp. 449–467.
conference:
end_date: 2018-07-17
location: Oxford, United Kingdom
name: 'CAV: Computer Aided Verification'
start_date: 2018-07-14
date_created: 2018-12-11T11:44:51Z
date_published: 2018-07-18T00:00:00Z
date_updated: 2023-09-15T12:12:08Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-96145-3_24
external_id:
isi:
- '000491481600024'
file:
- access_level: open_access
checksum: fd95e8026deacef3dc752a733bb9355f
content_type: application/pdf
creator: dernst
date_created: 2018-12-17T15:57:06Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5718'
file_name: 2018_LNCS_Kong.pdf
file_size: 5591566
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 10981'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '07'
oa: 1
oa_version: Published Version
page: 449 - 467
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '7781'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachable set over-approximation for nonlinear systems using piecewise barrier
tubes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10981
year: '2018'
...
---
_id: '434'
abstract:
- lang: eng
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.
article_processing_charge: No
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Huobing
full_name: Song, Huobing
last_name: Song
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Rui
full_name: Wang, Rui
last_name: Wang
- first_name: Yong
full_name: Guan, Yong
last_name: Guan
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
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
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
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.
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.
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.
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.
date_created: 2018-12-11T11:46:27Z
date_published: 2018-01-01T00:00:00Z
date_updated: 2023-09-18T08:12:49Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/TITS.2017.2778077
external_id:
isi:
- '000446651100020'
intvolume: ' 19'
isi: 1
issue: '10'
language:
- iso: eng
month: '01'
oa_version: None
page: 3320 - 3333
publication: IEEE Transactions on Intelligent Transportation Systems
publication_status: published
publisher: IEEE
publist_id: '7389'
quality_controlled: '1'
related_material:
record:
- id: '1205'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Safety-assured model-driven design of the multifunction vehicle bus controller
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 19
year: '2018'
...
---
_id: '663'
abstract:
- lang: eng
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. '
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Sergiy
full_name: Bogomolov, Sergiy
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
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'
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'
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.
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.
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.'
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.
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.
conference:
end_date: 2017-04-20
location: Pittsburgh, PA, United States
name: 'HSCC: Hybrid Systems Computation and Control '
start_date: 2017-04-18
date_created: 2018-12-11T11:47:47Z
date_published: 2017-04-01T00:00:00Z
date_updated: 2021-01-12T08:08:17Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3049797.3049814
file:
- access_level: open_access
checksum: b7667434cbf5b5f0ade3bea1dbe5bf63
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:20Z
date_updated: 2020-07-14T12:47:34Z
file_id: '4873'
file_name: IST-2017-817-v1+1_p163-kong.pdf
file_size: 1650530
relation: main_file
file_date_updated: 2020-07-14T12:47:34Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 163 - 172
publication: Proceedings of the 20th International Conference on Hybrid Systems
publication_identifier:
isbn:
- 978-145034590-3
publication_status: published
publisher: ACM
publist_id: '7067'
pubrep_id: '817'
quality_controlled: '1'
scopus_import: 1
status: public
title: Safety verification of nonlinear hybrid systems based on invariant clusters
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '647'
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.
alternative_title:
- LNCS
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
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'
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'
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.
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.'
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.'
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.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'FORMATS: Formal Modelling and Analysis of Timed Systems'
start_date: 2017-09-05
date_created: 2018-12-11T11:47:41Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-09-07T12:53:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_7
file:
- access_level: open_access
checksum: faf546914ba29bcf9974ee36b6b16750
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:38Z
date_updated: 2020-07-14T12:47:31Z
file_id: '4956'
file_name: IST-2017-831-v1+1_main.pdf
file_size: 3806864
relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 116 - 132
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-331965764-6
publication_status: published
publisher: Springer
publist_id: '7129'
pubrep_id: '831'
quality_controlled: '1'
related_material:
record:
- id: '6894'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Conic abstractions for hybrid systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: '10419 '
year: '2017'
...
---
_id: '479'
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
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"
alternative_title:
- Proceedings International Conference on Software Engineering
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Rui
full_name: Wang, Rui
last_name: Wang
- first_name: Mohamad
full_name: Hosseini, Mohamad
last_name: Hosseini
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
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'
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'
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.
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.
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.'
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.
conference:
end_date: 2016-05-22
location: Austin, TX, USA
name: 'ICSE: International Conference on Software Engineering'
start_date: 2016-05-14
date_created: 2018-12-11T11:46:42Z
date_published: 2016-05-14T00:00:00Z
date_updated: 2021-01-12T08:00:55Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2889160.2889233
language:
- iso: eng
month: '05'
oa_version: None
page: 112 - 121
publication: 'Proceedings of the 38th International Conference on Software Engineering
Companion '
publication_status: published
publisher: IEEE
publist_id: '7341'
quality_controlled: '1'
scopus_import: 1
status: public
title: Use runtime verification to improve the quality of medical care practice
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1205'
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.
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"
alternative_title:
- LNCS
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Houbing
full_name: Song, Houbing
last_name: Song
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ming
full_name: Gu, Ming
last_name: Gu
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
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'
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'
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.
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.'
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.'
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.
conference:
end_date: 2016-11-11
location: Limassol, Cyprus
name: 'FM: International Symposium on Formal Methods'
start_date: 2016-11-09
date_created: 2018-12-11T11:50:42Z
date_published: 2016-11-08T00:00:00Z
date_updated: 2023-09-18T08:12:48Z
day: '08'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-319-48989-6_47
file:
- access_level: open_access
checksum: fea0b3fae9a2a42e8bfec59840e30d8c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:13Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4673'
file_name: IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf
file_size: 281501
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9995'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 757 - 763
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '6144'
pubrep_id: '783'
quality_controlled: '1'
related_material:
record:
- id: '434'
relation: later_version
status: public
scopus_import: 1
status: public
title: Safety assured formal model driven design of the multifunction vehicle bus
controller
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9995
year: '2016'
...
---
_id: '1227'
abstract:
- lang: eng
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.
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).
alternative_title:
- LNCS
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
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'
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'
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.
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.'
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.'
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.
short: H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C.
Schilling, in:, Springer, 2016, pp. 128–144.
conference:
end_date: 2016-10-21
location: Grenoble, France
name: 'HSB: Hybrid Systems Biology'
start_date: 2016-10-20
date_created: 2018-12-11T11:50:49Z
date_published: 2016-09-25T00:00:00Z
date_updated: 2021-01-12T06:49:13Z
day: '25'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-47151-8_9
file:
- access_level: open_access
checksum: 994e164b558c47bacf8dc066dd27c8fc
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:49Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4840'
file_name: IST-2017-781-v1+1_main.pdf
file_size: 683955
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9957'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 128 - 144
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '6107'
pubrep_id: '781'
quality_controlled: '1'
scopus_import: 1
status: public
title: Discrete abstraction of multiaffine systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9957
year: '2016'
...
---
_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.
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.
article_number: '7461337'
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Yixiao
full_name: Yang, Yixiao
last_name: Yang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ming
full_name: Gu, Ming
last_name: Gu
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
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'
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'
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.'
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.'
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.'
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.'
short: Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
start_date: 2016-04-11
date_created: 2018-12-11T11:50:58Z
date_published: 2016-04-27T00:00:00Z
date_updated: 2021-01-12T06:49:26Z
day: '27'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1109/RTAS.2016.7461337
file:
- access_level: open_access
checksum: 42f0462911cc9957f2356b12fb33b4b6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:31Z
date_updated: 2020-07-14T12:44:41Z
file_id: '4949'
file_name: IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf
file_size: 1293599
relation: main_file
file_date_updated: 2020-07-14T12:44:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
publication_status: published
publisher: IEEE
publist_id: '6069'
pubrep_id: '780'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'From stateflow simulation to verified implementation: A verification approach
and a real-time train controller design'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1605'
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.
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/).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Grégory
full_name: Batt, Grégory
last_name: Batt
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
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'
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.
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.'
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.
short: S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:,
Springer, 2015, pp. 19–35.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2021-01-12T06:51:56Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 3aab260f3f34641d622030ba22645b3e
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:43:19Z
date_updated: 2020-07-14T12:45:05Z
file_id: '7851'
file_name: 2015_LNCS_Bogomolov.pdf
file_size: 1053207
relation: main_file
file_date_updated: 2020-07-14T12:45:05Z
has_accepted_license: '1'
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 19 - 35
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5561'
quality_controlled: '1'
scopus_import: 1
status: public
title: Abstraction-based parameter synthesis for multiaffine systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...