Automatic extraction of safety properties from Lustre programs

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/112694
Download file(s):
There are no files associated with this item.
Type: Examensarbete för masterexamen
Master Thesis
Title: Automatic extraction of safety properties from Lustre programs
Authors: Fei, Zhennan
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.
Keywords: Programvaruteknik;Software Engineering
Issue Date: 2009
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/112694
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.