Automatic extraction of safety properties from Lustre programs

Abstract

Lustre is a synchronous data‐flow language for developing reactive systems. Developed and maintained by Verimag, Lustre has been the core language of the industrial environment SCADE, developed by Esterel‐Technologies and used particularly by Schneider‐Electric for the nuclear power plant control software and Airbus for the on‐board software of Airbus A340/600 and A380.Since most reactive systems are safety critical, the validation and verification is particularly essential. The subject of the thesis focuses on the validation of reactive systems described in the synchronous data‐flow language Lustre. During the verification, the model checker takes a Lustre program and two observers - respective describing the intended properties and the assumptions about the environment, and performs the validation on a finite state abstraction of the system. Generally, both of the intended behaviors of the program and the assumptions about the environment consist of properties and almost all of them are safety properties. Nowadays, when verifying a Lustre program, Lustre programs usually have to extract the safety properties manually, which is can be inefficient and error‐prone. According to this, a framework in the thesis is produced to automatically extract simple numeric and Boolean properties from Lustre programs. The safety properties extracted by the framework are expressed formally to be used to construct the synchronous observer as the intended behavior of the Lustre program or the assumption about the environment and verified by model checkers in the later stage.