Abstract | ||
---|---|---|
In this paper we describe the ForSpec Temporal Logic (FTL), the new temporal property-specification logic of ForSpec, Intel's new formal specification language. The key features of FTL are as follows: it is a linear temporal logic, based on Pnueli's LTL, it is based on a rich set of logical and arithmetical operations on bit vectors to describe state properties, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, it enables the user to express properties about the past, and it includes constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of hardware design. |
Year | DOI | Venue |
---|---|---|
2002 | 10.1007/3-540-46002-0_21 | Tools and Algorithms for Construction and Analysis of Systems |
Keywords | Field | DocType |
linear temporal logic,new temporal property-specification logic,temporal connective,ForSpec Temporal Logic,new formal specification language,regular event,regular sequence,Boolean event,arithmetical operation,bit vector,New Temporal Property-Specification Language | Computation tree logic,Temporal logic of actions,Programming language,Interval temporal logic,Computer science,Theoretical computer science,Linear temporal logic,Property Specification Language,Boolean algebra,Linear logic,Temporal logic | Conference |
Volume | ISSN | ISBN |
2280 | 0302-9743 | 3-540-43419-4 |
Citations | PageRank | References |
5 | 0.54 | 0 |
Authors | ||
12 |
Name | Order | Citations | PageRank |
---|---|---|---|
Roy Armoni | 1 | 63 | 6.63 |
Limor Fix | 2 | 13 | 1.19 |
Alon Flaisher | 3 | 5 | 0.54 |
Rob Gerth | 4 | 46 | 15.14 |
Boris Ginsburg | 5 | 5 | 4.26 |
Tomer Kanza | 6 | 5 | 0.54 |
Avner Landver | 7 | 5 | 0.54 |
Sela Mador-Haim | 8 | 5 | 0.54 |
Eli Singerman | 9 | 5 | 0.54 |
Andreas Tiemeyer | 10 | 5 | 0.54 |
Moshe Y. Vardi | 11 | 529 | 73.64 |
Yael Zbar | 12 | 5 | 0.54 |