Name
Abstract | ||
|---|---|---|
We describe the verification methods and tools we are currently developing around the language ESTEREL. This language is dedicated for the development of synchronous reactive systems such as hardware or software controllers for which the control handling aspects are predominant. The language has a strong mathematical semantics in terms of Finite State Machines. Automatic verification is then possible on this model in which we represent exhaustively all the possible behaviors of a system. Our methods are based on model minimization coupled with unrelevant behaviors masking and model checking techniques to verify correctness properties like safety and liveness ones by means of synchronous observers |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/BFb0028770 | CAV |
Keywords | Field | DocType |
esterel verification environment,reactive system,finite state machine,model checking | Programming language,Model checking,Computer science,Correctness,Denotational semantics,Finite-state machine,Esterel,Reactive system,Formal verification,Liveness | Conference |
Volume | ISSN | ISBN |
1427 | 0302-9743 | 3-540-64608-6 |
Citations | PageRank | References |
40 | 2.59 | 5 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Amar Bouali | 1 | 154 | 12.50 |