Incremental Verification of Inductive Invariants for the Run-Time Evolution of Self-Adaptive Software-Intensive Systems (bibtex)
by ,
Abstract:
The safe run-time evolution of complex software-intensive systems requires that the impact of changes can be predicted at run-time. In this paper we consider the specific case of self-adaptive software-intensive systems using an example for the coordination of autonomous vehicles. We show how incremental run-time checks can verify that changes in the rule set which governs the distributed rule-based self-adaptive behavior provides the required safety properties. We demonstrate how an existing verification technique for invariant checking is turned into an incremental one. We discuss the theoretical complexity of the incremental verification checks and also present some first evaluation results.
Reference:
Incremental Verification of Inductive Invariants for the Run-Time Evolution of Self-Adaptive Software-Intensive Systems (Basil Becker, Holger Giese), In Proc. 1st International Workshop on Automated engineeRing of Autonomous and run-tiMe evolvIng Systems (ARAMIS), IEEE Computer Society Press, 2008.
Bibtex Entry:
@InProceedings{BeckerGiese08b,
AUTHOR = {Becker, Basil and Giese, Holger},
TITLE = {{Incremental Verification of Inductive Invariants for the Run-Time Evolution of Self-Adaptive Software-Intensive Systems}},
YEAR = {2008},
BOOKTITLE = {Proc. 1st International Workshop on Automated engineeRing of Autonomous and run-tiMe evolvIng Systems (ARAMIS)},
PAGES = {33-40},
PUBLISHER = {IEEE Computer Society Press},
PDF = {uploads/pdf/BeckerGiese08b_aramis08.pdf},
OPTacc_pdf = {},
ABSTRACT = {The safe run-time evolution of complex software-intensive systems requires that the impact of changes can be predicted at run-time. In this paper we consider the specific case of self-adaptive software-intensive systems using an example for the coordination of autonomous vehicles. We show how incremental run-time checks can verify that changes in the rule set which governs the distributed rule-based self-adaptive behavior provides the required safety properties. We demonstrate how an existing verification technique for invariant checking is turned into an incremental one. We discuss the theoretical complexity of the incremental verification checks and also present some first evaluation results.}
}
Powered by bibtexbrowser