WCSE

Extracting Data Invariants from Promela

Abstract— Data Invariants are the essential conditions that hold during the execution of program. In software verification, the data invariants should be assessed to ensure the correctness of the system behavior. Unfortunately, it has been difficult to indicate the data invariants in a given source code. In this paper, we aim to extract relevant data invariants automatically from the Promela source code. The Promela code is typically used as the software modelling language in model checking tool, called SPIN model checker. We exploit the program slicing technique to minimize the Promela source code and track all of the relevant active bound variables to recognize the data invariants in term of their possible and valid bounded values. The data invariants are written in propositions and their temporal logic formula (LTL formula). The resulting data invariants are checked using model checking tool.

Index Terms— data invariants, LTL, program slicing, dynamic slicing, promela, SPIN, formal verification

Wisut Suksribangteuy, Wiwat Vatanawood
Department of Computer Engineering, Chulalongkorn University, THAILAND

[Download]

Cite: Wisut Suksribangteuy, Wiwat Vatanawood, "Extracting Data Invariants from Promela," Proceedings of 2018 the 8th International Workshop on Computer Science and Engineering, pp. 647-651, Bangkok, 28-30 June, 2018.