Name
Abstract | ||
|---|---|---|
In this paper we propose an approach to automatically produce test cases allowing to check the satisfiability of a linear property on a given implementation. Linear properties can be expressed by formulas of temporal logic. An observer is built from each formula. An observer is a finite automaton on infinite sequences. Of course, testing the satisfiability of an infinite sequence is not possible. Thus, we introduce the notion of bounded properties. Test cases are generated from a (possibly partial) specification of the IUT and the property to validate is expressed by a parameterised automaton on infinite words. This approach is formally defined, and a practical test generation algorithm is sketched. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-24617-6_11 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
finite automaton,satisfiability,property testing,temporal logic | Discrete mathematics,Sequence,Satisfiability,Automaton,Finite-state machine,Test case,Temporal logic,Observer (quantum physics),Mathematics,Bounded function | Conference |
Volume | ISSN | Citations |
2931 | 0302-9743 | 15 |
PageRank | References | Authors |
0.70 | 9 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean-Claude Fernandez | 1 | 184 | 8.53 |
| Laurent Mounier | 2 | 1187 | 79.54 |
| Cyril Pachon | 3 | 33 | 1.60 |