Software Reliability Analysis Using Weakest Preconditions in Linear Assignment Programs

doi:10.1109/TSE.2016.2521379

Return

Software Reliability Analysis Using Weakest Preconditions in Linear Assignment Programs

2016-09-01

PRE

DOI：10.1109/TSE.2016.2521379

Original

Original request for help

Save

Abstract

En 中文

Weakest preconditions derived from triple axiomatic semantics have been widely used to prove the correctness of programs. They can also be applied to evaluate the reliability of software. However, deducing a weakest precondition, as well as determining its propagation path, encounters challenges such as unknown constraint conditions, symbol computation and means of representation. To address these challenges, in this paper, we utilize the disjunctive normal form of if-else branch structure to capture reasonable propagation paths of the weakest precondition. Meanwhile, by removing the sequential dependencies, we demonstrate how to get the weakest precondition of loop-structure by leveraging program function. Moreover, we extensively explore three modeling characteristics (i.e., path extension, innermost connection and condition leap) for deducing the weakest precondition of structured programs. Finally, taking the definition of program node and storage structure of weakest precondition as bases, we design a serial of modeling algorithms. Based on symbol computation and recursive call technology with Depth-First Search (DFS), our algorithms can not only be used to deduce the weakest precondition, but also to capture the propagate path of the weakest precondition. Experiments illustrate the efficacy and effectiveness of our proposed models and designed deductive algorithms.

Keywords:

Weakest precondition

path extension

innermost connection

condition leap

node

cell-structure

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.