Monitoring Assumptions in Assume-Guarantee Contracts
Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run time. This is because assumptions about the environment cannot be discharged until the environment is fixed. An intuitive...
Main Authors: | , , , |
---|---|
Format: | Conference Object |
Language: | unknown |
Published: |
2016
|
Subjects: | |
Online Access: | https://repository.upenn.edu/handle/20.500.14332/6902 https://hdl.handle.net/20.500.14332/6902 |
id |
ftunivpenn:oai:repository.upenn.edu:20.500.14332/6902 |
---|---|
record_format |
openpolar |
spelling |
ftunivpenn:oai:repository.upenn.edu:20.500.14332/6902 2024-02-04T10:01:31+01:00 Monitoring Assumptions in Assume-Guarantee Contracts Sokolsky, Oleg Zhang, Teng Lee, Insup McDougall, Michael 2016-06-01 application/pdf https://repository.upenn.edu/handle/20.500.14332/6902 https://hdl.handle.net/20.500.14332/6902 unknown https://repository.upenn.edu/handle/20.500.14332/6902 46 53 824 Departmental Papers (CIS) Workshop on Pre- and Post-Deployment Verification Techniques (PrePost@IFM) true published CPS Formal Methods Computer Engineering Computer Sciences Presentation 2016 ftunivpenn https://doi.org/20.500.14332/6902 2024-01-06T23:28:45Z Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run time. This is because assumptions about the environment cannot be discharged until the environment is fixed. An intuitive approach is to complement pre-deployment verification of guarantees, up to the assumptions, with post-deployment monitoring of environment behavior to check that the assumptions are satisfied at run time. Such a monitor is typically implemented by instrumenting the application code of the component. An additional challenge for the monitoring step is that environment behaviors are typically obtained through an I/O library, which may alter the component’s view of the input format. This transformation requires us to introduce a second pre-deployment verification step to ensure that alarms raised by the monitor would indeed correspond to violations of the environment assumptions. In this paper, we describe an approach for constructing monitors and verifying them against the component assumption. We also discuss limitations of instrumentation-based monitoring and potential ways to overcome it. Workshop on Pre- and Post-Deployment Verification Techniques (PrePost@IFM), pp. 46--53, Reykjavik, Iceland, June 2016. Conference Object Iceland University of Pennsylvania: ScholaryCommons@Penn |
institution |
Open Polar |
collection |
University of Pennsylvania: ScholaryCommons@Penn |
op_collection_id |
ftunivpenn |
language |
unknown |
topic |
CPS Formal Methods Computer Engineering Computer Sciences |
spellingShingle |
CPS Formal Methods Computer Engineering Computer Sciences Sokolsky, Oleg Zhang, Teng Lee, Insup McDougall, Michael Monitoring Assumptions in Assume-Guarantee Contracts |
topic_facet |
CPS Formal Methods Computer Engineering Computer Sciences |
description |
Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run time. This is because assumptions about the environment cannot be discharged until the environment is fixed. An intuitive approach is to complement pre-deployment verification of guarantees, up to the assumptions, with post-deployment monitoring of environment behavior to check that the assumptions are satisfied at run time. Such a monitor is typically implemented by instrumenting the application code of the component. An additional challenge for the monitoring step is that environment behaviors are typically obtained through an I/O library, which may alter the component’s view of the input format. This transformation requires us to introduce a second pre-deployment verification step to ensure that alarms raised by the monitor would indeed correspond to violations of the environment assumptions. In this paper, we describe an approach for constructing monitors and verifying them against the component assumption. We also discuss limitations of instrumentation-based monitoring and potential ways to overcome it. Workshop on Pre- and Post-Deployment Verification Techniques (PrePost@IFM), pp. 46--53, Reykjavik, Iceland, June 2016. |
format |
Conference Object |
author |
Sokolsky, Oleg Zhang, Teng Lee, Insup McDougall, Michael |
author_facet |
Sokolsky, Oleg Zhang, Teng Lee, Insup McDougall, Michael |
author_sort |
Sokolsky, Oleg |
title |
Monitoring Assumptions in Assume-Guarantee Contracts |
title_short |
Monitoring Assumptions in Assume-Guarantee Contracts |
title_full |
Monitoring Assumptions in Assume-Guarantee Contracts |
title_fullStr |
Monitoring Assumptions in Assume-Guarantee Contracts |
title_full_unstemmed |
Monitoring Assumptions in Assume-Guarantee Contracts |
title_sort |
monitoring assumptions in assume-guarantee contracts |
publishDate |
2016 |
url |
https://repository.upenn.edu/handle/20.500.14332/6902 https://hdl.handle.net/20.500.14332/6902 |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
46 53 824 Departmental Papers (CIS) Workshop on Pre- and Post-Deployment Verification Techniques (PrePost@IFM) true published |
op_relation |
https://repository.upenn.edu/handle/20.500.14332/6902 |
op_doi |
https://doi.org/20.500.14332/6902 |
_version_ |
1789967474659164160 |