Extending Structural Test Coverage Criteria for Lustre Programs with Multi-clock Operators

Lustre is a formal synchronous declarative language widely used for modeling and specifying safety-critical applications in the elds of avionics, transportation or energy production. Testing this kind of applications is an important and demanding task during the development process. It mainly consists in generating test data and measuring the achieved coverage. A hierarchy of structural coverage criteria for Lustre programs has been recently dened to assess the thoroughness of a given test set. They are based on the operator network, which is the graphical representation of a Lustre program and depicts the way that input ows are transformed into output ows through their propagation along the program paths. The above criteria denition aimed at demonstrating the opportunity of such a coverage assessment approach but doesn't deal with all the language constructions. In particular, the use of multiple clocks has not been taken into account. In this paper, we extend the criteria to pro...

• Type: Conference
• Year: 2008
• Where: FMICS
• Authors: Virginia Papailiopoulou, Laya Madani, Lydie du Bousquet, Ioannis Parissis
• Keywords: FMICS 2008, Formal Methods, Lustre Program, Multiple Clocks, Structural Coverage Criteria