Paper Info
Title
Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing
Abstract
This paper surveys the techniques and tools developped for the validation of reactive systems described in the synchronous data-flow language Lustre [HCRP91]. These techniques are based on the specification of safety properties, by means of synchronous observers. The modelchecker Lesar [RHR91] takes a Lustre program, and two observers -- respectively describing the expected properties of the program, and the assumptions about the system environment under which these properties are intended to hold --, and performs the verification on a finite state (Boolean) abstraction of the system. Recent work concerns extensions towards simple numerical aspects, which are ignored in the basic tool. Provided with the same kind of observers, the tool Lurette [RWNH98] is able to automatically generate test sequences satisfying the environment assumptions, and to run the test while checking the satisfaction of the specified properties.
Year
DOI
Venue
1999
10.1007/3-540-46674-6_1
ASIAN
Keywords
Field
DocType
reactive system,synchronous data-flow language,synchronous reactive systems,automatic testing,tool lurette,system environment,lustre program,expected property,basic tool,finite state,synchronous observer,environment assumption,formal verification
Programming language,Abstraction,Computer science,Algorithm,Automatic testing,Formal specification,Real-time operating system,Finite state,Lustre (mineralogy),Reactive system,Distributed computing,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-66856-X
22
1.21
References 
Authors
16
2
Name
Order
Citations
PageRank
Nicolas Halbwachs13957426.43
Pascal Raymond256753.53