Title :
Expressing and implementing operational profiles for reactive software validation
Author :
du Bousquet, L. ; Ouabdesselam, F. ; Richier, J.L.
Author_Institution :
LSR-IMAG, Saint Martin d´´Heres, France
Abstract :
Lutess is a tool that we developed for testing reactive synchronous software and which is being used in different industrial contexts. It offers several formal testing methods with automatic generation of test data from the environment specification. Lutess provides also an approach to assign a probability to the next event issued by the environment. However, a Lutess´ user faces the problem of expressing operational profiles with sophisticated and varying probability assignments to software inputs, in a format directly usable by Lutess. The paper concentrates on how to express operational profiles for specifications which are implemented as binary decision diagrams
Keywords :
binary decision diagrams; formal specification; probability; program testing; program verification; Lutess; Lutess user; automatic generation; binary decision diagrams; environment specification; formal testing methods; industrial contexts; operational profiles; probability; probability assignments; reactive software validation; reactive synchronous software testing; software inputs; test data; Automata; Automatic testing; Boolean functions; Data structures; Input variables; Maintenance; Postal services; Read only memory; Software reliability; Software safety;
Conference_Titel :
Software Reliability Engineering, 1998. Proceedings. The Ninth International Symposium on
Conference_Location :
Paderborn
Print_ISBN :
0-8186-8991-9
DOI :
10.1109/ISSRE.1998.730885