Formal specification and automatic validation of interactive software

摘要

The purpose of this paper is to present the research results on User Interface Systems (UIS) automatic validation, based on Lustre language formal specification. It describes the software prototype we have developed, and which allows to generate a formal model of the UIS and to automatically verify properties on it. It then proposes axes of optimization in order to validate this prototype on significant operational space ground segment UIS.