The ForSpec Temporal Logic: A New Temporal Property-Specification Language Export

@inproceedings{citeulike:3328505, 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. 1}, address = {London, UK}, author = {Armoni, Roy and Fix, Limor and Flaisher, Alon and Gerth, Rob and Ginsburg, Boris and Kanza, Tomer and Landver, Avner and Haim, Sela M. and Singerman, Eli and Tiemeyer, Andreas and Vardi, Moshe Y. and Zbar, Yael}, booktitle = {TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, citeulike-article-id = {3328505}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=646486.694616}, isbn = {3-540-43419-4}, keywords = {temporal-logic}, pages = {296--211}, posted-at = {2008-09-24 08:25:56}, priority = {2}, publisher = {Springer-Verlag}, title = {The ForSpec Temporal Logic: A New Temporal Property-Specification Language}, url = {http://portal.acm.org/citation.cfm?id=646486.694616}, year = {2002} }

TY - CONF ID - citeulike:3328505 L3 - citeulike-article-id:3328505 N2 - 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. 1 SN - 3-540-43419-4 AD - London, UK EP - 211 TI - The ForSpec Temporal Logic: A New Temporal Property-Specification Language PB - Springer-Verlag T2 - TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems SP - 296 KW - temporal-logic AU - Armoni, Roy AU - Fix, Limor AU - Flaisher, Alon AU - Gerth, Rob AU - Ginsburg, Boris AU - Kanza, Tomer AU - Landver, Avner AU - Haim, Sela AU - Singerman, Eli AU - Tiemeyer, Andreas AU - Vardi, Moshe AU - Zbar, Yael PY - 2002/// UR - http://portal.acm.org/citation.cfm?id=646486.694616 ER -