RV-enabled framework for self-adaptive software / Teng Zhang.

Format:

Book

Thesis/Dissertation

Author/Creator:

Zhang, Teng, author.

Contributor:

Sokolsky, Oleg, degree supervisor.

Lee, Insup, degree supervisor.

University of Pennsylvania. Department of Computer and Information Science, degree granting institution.

Language:

English

Subjects (All):

Computer science.

Computer engineering.

Information technology.

Computer and Information Science--Penn dissertations.

Penn dissertations--Computer and Information Science.

Local Subjects:

Computer science.

Computer engineering.

Information technology.

Computer and Information Science--Penn dissertations.

Penn dissertations--Computer and Information Science.

Physical Description:

1 online resource (192 pages)

Contained In:

Dissertations Abstracts International 83-08B.

Place of Publication:

[Philadelphia, Pennsylvania] : University of Pennsylvania ; Ann Arbor : ProQuest Dissertations & Theses, 2021.

Language Note:

English

System Details:

Mode of access: World Wide Web.

Summary:

Software systems keep increasing in scale and complexity, requiring ever more effort to design, build, test, and deploy. Systems are integrated from separately developed modules. Over the life of a system, individual modules may be updated, which may allow incompatibilities between modules to slip in. Consequently, many faults in a software system are often discovered after the system is built and deployed. Runtime verification (RV) is a collection of dynamic techniques for detecting faults of software systems. An executable monitor is constructed from a formally specified property of the system being checked (denoted as the target system) and is run over a stream of observations (events) to check whether the property is satisfied or not. Although existing tools are able to specify and monitor properties efficiently, it is still challenging to apply RV to large-scale real-world applications. From the perspective of monitoring requirements, we need a formalism that can describe both high and low-level behaviors of the target system. Complexity of the target program also brings some issues. For instance, it may contain a set of loosely-coupled components which may be added or removed dynamically. Correspondingly, monitoring requirements are often defined upon asynchronous observations that carry data of which the domain scale up along with expansion of the target system. How to conveniently specify these properties and generate monitors that can check them efficiently is a challenge. Beyond detecting faults, self-adaptive software is desirable for tolerating faults or unexpected environment changes during execution. By equipping monitors with reflexive adaptation actions, runtime enforcement (RE) can be used to improve robustness of the system. However, there is little work on analyzing possible interference between the implementation of adaptation actions and the target program. In this thesis, we present SMEDL, a RV framework using a specification language designed for high usability with respect to expressiveness, efficiency and flexible deployment. The property specification is composed of a set of communicating monitors described in the form of EFSMs (extend finite state machines). High-level properties can be straightforwardly transformed into SMEDL specifications while actions can be specified in transitions to express low-level imperative behaviors. Deployment of monitors can be explicitly specified to support both centralized and distributed software. Based on dynamically scalable monitor structure, we propose a novel method to efficiently check parametric properties that rely on the data events carry. To tackle challenges of monitoring timing properties in an asynchronous environment, we propose a conceptual monitor architecture that clearly separates monitoring of time intervals from the rest of property checking.To support software adaptation, we extend the SMEDL framework to specify enforcement specifications, generate implementations and instrument them into the target system. Analysis of interference between the adaptation implementation and the target system can be performed statically based on Hoare-logic. Instead of building a whole new proof for the target system globally, we present a method to generate local proof obligations for better scalability.

Notes:

Source: Dissertations Abstracts International, Volume: 83-08, Section: B.

Advisors: Sokolsky, Oleg; Lee, Insup; Committee members: Naik, Mayur; Alur, Rajeev; Weirich, Stephanie; Havelund, Klaus.

Department: Computer and Information Science.

Ph.D. University of Pennsylvania 2021.

Local Notes:

School code: 0175

ISBN:

9798780680420

Access Restriction:

Restricted for use by site license.

This item must not be sold to any third party vendors.