A formal approach to providing assurance to dynamically adaptive software.

摘要

Increasingly, software must adapt its behavior in response to the changes in its run-time environment and user requirements in order to upgrade services, to harden security, or to improve performance. In order for adaptive software to be used in safety critical and mission critical systems, they must be trusted. Adaptive software assurance must be addressed at different stages of the software development process, including the requirements analysis phase, the design phase, and the implementation phase. An adaptation-oriented systematic software development process that applies formal methods throughout the process can be used to provide assurance to adaptive systems. This dissertation introduces a number of specification languages, modeling techniques, and model checking techniques to support a systematic approach to providing assurance to adaptive software from requirements through design and implementation phases. We introduce A-LTL, an adaptation extension to LTL, and a goal-based requirements analysis technique to formally specify adaptation requirements. We develop a model-based design technique to describe the designs that satisfy the adaptation requirements. Verification techniques are proposed to ensure that the artifacts produced in later phases conform to artifacts produced in earlier ones. Safe adaptation protocols and model checking techniques are applied to ensure that these designs are correctly followed and the requirements are satisfied in the implementation. We have applied our techniques to a number of case studies involving adaptive mobile computing applications.