Title
The ForSpec Temporal Logic: A New Temporal Property-Specification Language
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 Armoni1636.63
Limor Fix2131.19
Alon Flaisher350.54
Rob Gerth44615.14
Boris Ginsburg554.26
Tomer Kanza650.54
Avner Landver750.54
Sela Mador-Haim850.54
Eli Singerman950.54
Andreas Tiemeyer1050.54
Moshe Y. Vardi1152973.64
Yael Zbar1250.54