عنوان

Synthesis of Specifications and Refinement Maps for Real-time Object Code Verification

Number

TLpq2408897721

.Language of Text, Soundtrack etc

انگلیسی

Title Proper

Synthesis of Specifications and Refinement Maps for Real-time Object Code Verification

General Material Designation

[Thesis]

First Statement of Responsibility

Al-Qtiemat, Eman Mohammad

Subsequent Statement of Responsibility

Srinivasan, Sudarshan K.

Name of Publisher, Distributor, etc.

North Dakota State University

Date of Publication, Distribution, etc.

2020

Specific Material Designation and Extent of Item

113

Dissertation or thesis details and type of degree

Ph.D.

Body granting the degree

North Dakota State University

Text preceding or following the note

2020

Text of Note

Formal verification methods have been shown to be very effective in finding corner-case bugs and ensuring the safety of embedded software systems. The use of formal verification requires a specification, which is typically a high-level mathematical model that defines the correct behavior of the system to be verified. However, embedded software requirements are typically described in natural language. Transforming these requirements into formal specifications is currently a big gap. While there is some work in this area, we proposed solutions to address this gap in the context of refinement-based verification, a class of formal methods that have shown to be effective for embedded object code verification. The proposed approach also addresses both functional and timing requirements and has been demonstrated in the context of safety requirements for software control of infusion pumps. The next step in the verification process is to develop the refinement map, which is a mapping function that can relate an implementation state (in this context, the state of the object code program to be verified) with the specification state. Actually, constructing refinement maps often requires deep understanding and intuitions about the specification and implementation, it is shown very difficult to construct refinement maps manually. To go over this obstacle, the construction of refinement maps should be automated. As a first step toward the automation process, we manually developed refinement maps for various safety properties concerning the software control operation of infusion pumps. In addition, we identified possible generic templates for the construction of refinement maps. Recently, synthesizing procedures of refinement maps for functional and timing specifications are proposed. The proposed work develops a process that significantly increases the automation in the generation of these refinement maps. The refinement maps can then be used for refinement-based verification. This automation procedure has been successfully applied on the transformed safety requirements in the first part of our work. This approach is based on the identified generic refinement map templates which can be increased in the future as the application required.

Computer engineering

Computer science

Electrical engineering

Al-Qtiemat, Eman Mohammad

Srinivasan, Sudarshan K.

Electronic name

p

[Thesis]

276903

a

Y