Extracting scalable program models for TLA model checking

Abstract: Program verification has long been of interest to researchers and practitioners for its role in asserting reliability in critical systems. Many such systems feature reactive behavior, where temporal properties are of interest. Consequently, a number of systems and program verification tools for dealing with temporal logic have been developed. One such is TLA, whose main purpose is to verify temporal properties of systems using model checking. A TLA model is determined by a logical formula that describes all possible behaviors of a system. TLA is primarily used to verify abstract system designs, as it is considered ill-suited for implementation code in real programming languages. This thesis investigates how TLA models can be extracted from real code, in order to verify temporal properties of the code. The main problem is getting the model size to scale well with the size of the code, while still being representative. The paper presents a general method for achieving this, which utilizes deductive verification to abstract away unnecessary implementation details from the model. Specifically, blocks which can be considered atomic are identified in the original code and replaced with Hoare-style assertions representing only the data transformation performed in the block. The result can then be translated to a more compact TLA model. The assertions, known as block contracts, are verified separately using deductive verification, ensuring the model remains representative. We successfully instantiate the method on a simple C program, using the tool Frama-C to perform deductive verification on blocks of code and translating the result to a TLA model in several steps. The PlusCal algorithm language is used as an intermediary to simplify the translation, and block contracts are successfully translated to TLA using a simple encoding. The results show promise, but there is future work to be done.