Quantitative reactive modeling and verification

T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.

Download
OA 570.36 KB

Journal Article | Published | English
Department
Abstract
Formal verification aims to improve the quality of software by detecting errors before they do harm. At the basis of formal verification is the logical notion of correctness, which purports to capture whether or not a program behaves as desired. We suggest that the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria. We therefore propose to introduce quantitative fitness measures for programs, specifically for measuring the function, performance, and robustness of reactive programs such as concurrent processes. This article describes the goals of the ERC Advanced Investigator Project QUAREM. The project aims to build and evaluate a theory of quantitative fitness measures for reactive models. Such a theory must strive to obtain quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction and abstraction refinement, model checking, and synthesis. The theory will be evaluated not only in the context of software and hardware engineering, but also in the context of systems biology. In particular, we will use the quantitative reactive models and fitness measures developed in this project for testing hypotheses about the mechanisms behind data from biological experiments.
Publishing Year
Date Published
2013-10-05
Journal Title
Computer Science Research and Development
Acknowledgement
The author thanks the European Research Council (ERC) for supporting this project. Above all, the author thanks his many wonderful collaborators on the topic of this project.
Volume
28
Issue
4
Page
331 - 344
IST-REx-ID

Cite this

Henzinger TA. Quantitative reactive modeling and verification. Computer Science Research and Development. 2013;28(4):331-344. doi:10.1007/s00450-013-0251-7
Henzinger, T. A. (2013). Quantitative reactive modeling and verification. Computer Science Research and Development, 28(4), 331–344. https://doi.org/10.1007/s00450-013-0251-7
Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer Science Research and Development 28, no. 4 (2013): 331–44. https://doi.org/10.1007/s00450-013-0251-7.
T. A. Henzinger, “Quantitative reactive modeling and verification,” Computer Science Research and Development, vol. 28, no. 4, pp. 331–344, 2013.
Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer Science Research and Development. 28(4), 331–344.
Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer Science Research and Development, vol. 28, no. 4, Springer, 2013, pp. 331–44, doi:10.1007/s00450-013-0251-7.
All files available under the following license(s):
Creative Commons License:
CC-BYCreative Commons Attribution 4.0 International Public License (CC-BY 4.0)
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T10:17:51Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar