Quantitative reactive modeling and verification

Henzinger, Thomas A (2013) Quantitative reactive modeling and verification. Computer Science Research and Development, 28 (4). pp. 331-344. ISSN 1865-2034

[img] Text
s00450-013-0251-7.pdf - Published Version
Available under License Creative Commons Attribution.
Download (556Kb)
Official URL: http://dx.doi.org/10.1007/s00450-013-0251-7


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.

Item Type: Article
DOI: 10.1007/s00450-013-0251-7
Uncontrolled Keywords: Formal methods, embedded systems, systems biology, Program verification
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
Research Group: Henzinger Group
SWORD Depositor: Sword Import User
Depositing User: Sword Import User
Date Deposited: 16 Aug 2016 12:07
Last Modified: 05 Sep 2017 14:23
URI: https://repository.ist.ac.at/id/eprint/626

Actions (login required)

View Item View Item