dc.contributor.author | Riley, Ian | |
dc.contributor.author | Jahan, Sharmin | |
dc.contributor.author | Marshall, Allen | |
dc.contributor.author | Walter, Charles | |
dc.contributor.author | Gamble, Rose F. | |
dc.date.accessioned | 2023-10-12T14:57:50Z | |
dc.date.available | 2023-10-12T14:57:50Z | |
dc.date.issued | 2021-02-22 | |
dc.identifier | oksd_riley_evaluating_verification_awareness_as_2021 | |
dc.identifier.citation | Riley, I., Jahan, S., Marshall, A., Walter, C., Gamble, R.F. (2021). Evaluating verification awareness as a method for assessing adaptation risk. Future Generation Computer Systems, 119, 110-135. https://doi.org/10.1016/j.future.2021.01.034 | |
dc.identifier.issn | 0167-739X | |
dc.identifier.uri | https://hdl.handle.net/11244/339845 | |
dc.description.abstract | Self-integration requires a system to be self-aware and self-protecting of its functionality and communication processes to mitigate interference in accomplishing its goals. Incorporating self-protection into a framework for reasoning about compliance with critical requirements is a major challenge when the system’s operational environment may have uncertainties resulting in runtime changes. The reasoning should be over a range of impacts and tradeoffs in order for the system to immediately address an issue, even if only partially or imperfectly. Assuming that critical requirements can be formally specified and embedded as part of system self-awareness, runtime verification often involves extensive on-board resources and state explosion, with minimal explanation of results. Model-checking partially mitigates runtime verification issues by abstracting the system operations and architecture. However, validating the consistency of a model given a runtime change is generally performed external to the system and translated back to the operational environment, which can be inefficient. | |
dc.description.abstract | This paper focuses on codifying and embedding verification awareness into a system. Verification awareness is a type of self-awareness related to reasoning about compliance with critical properties at runtime when a system adaptation is needed. The premise is that an adaptation that interferes with a design-time proof process for requirement compliance increases the risk that the original proof process cannot be reused. The greater the risk to limiting proof process reuse, the higher the probability that the requirement would be violated by the adaptation. The application of Rice’s 1953 theorem to this domain indicates that determining whether a given adaptation inherently inhibits proof reuse is undecidable, suggesting the heuristic, comparative approach based on proof meta-data that is part of our approach. To demonstrate our deployment of verification awareness, we predefine four adaptations that are all available to three distinct wearable simulations (stress, insulin delivery, and hearables). We capture meta-data from applying automated theorem proving to wearable requirements and assess the risk among the four adaptations for limiting the proof process reuse for each of their requirements. The results show that the adaptations affect proof process reuse differently on each wearable. We evaluate our reasoning framework by embedding checkpoints on requirement compliance within the wearable code and log the execution trace of each adaptation. The logs confirm that the adaptation selected by each wearable with the lowest risk of inhibiting proof process reuse for its requirements also causes the least number of requirement failures in execution. | |
dc.format | application/pdf | |
dc.language | en_US | |
dc.publisher | Elsevier | |
dc.relation.ispartof | Future Generation Computer Systems, 119 | |
dc.rights | This material has been previously published. In the Oklahoma State University Library's institutional repository this version is made available through the open access principles and the terms of agreement/consent between the author(s) and the publisher. The permission policy on the use, reproduction or distribution of the material falls under fair use for educational, scholarship, and research purposes. Contact Digital Resources and Discovery Services at lib-dls@okstate.edu or 405-744-9161 for further information. | |
dc.title | Evaluating verification awareness as a method for assessing adaptation risk | |
dc.date.updated | 2023-10-11T14:52:15Z | |
dc.note | open access status: Hybrid OA | |
osu.filename | oksd_riley_evaluating_verification_awareness_as_2021.pdf | |
dc.identifier.doi | 10.1016/j.future.2021.01.034 | |
dc.description.department | Computer Science | |
dc.type.genre | Article | |
dc.type.material | Text | |
dc.subject.keywords | theory of computation | |
dc.subject.keywords | information and computing sciences | |
dc.subject.keywords | software engineering | |
dc.subject.keywords | computer software | |
dc.subject.keywords | distributed computing | |
dc.subject.keywords | information systems | |
dc.subject.keywords | data management and data science | |
dc.subject.keywords | distributed computing and systems software | |
dc.identifier.author | ORCID: 0000-0003-1306-4591 (Jahan, Sharmin) | |
dc.identifier.author | ScopusID: 1941703 (Jahan, Sharmin) | |