Academic
Publications
The For-Spec temporal logic: A new temporal property-specification logic

The For-Spec temporal logic: A new temporal property-specification logic,R. Armoni,L. Fix,A. Flaisher,R. Gerth,B. Ginsburg,T. Kanza,A. Landver,S. Mado

The For-Spec temporal logic: A new temporal property-specification logic   (Citations: 21)
BibTex | RIS | RefWorks Download
Cumulative Annual
    • ...C++’s assert) [16], but the industry has recently recognized the need for temporal languages that can express properties related to ongoing behavior, such as p must hold until q is true [3]...
    • ...The property ìA call to function req() is followed within 3 clock cycles (of clock cl) by a notication of event ackî can be expressed as default clock = cl.posedge.notified; ALWAYS (req:call -> next[3] ack.notified)...
    • ...If the acknowledgment needs to be received within 3 delta cycles instead, all we need to do is change the clock expression: default clock=(kernel_phase=delta_notify); ALWAYS (req:call -> next[3] ack.notified)...

    Deian Tabakovet al. A Temporal Language for SystemC

    • ...Recent industrial-strength property-specica tion languages such as Sugar [2], ForSpec [1], and the recent standard PSL 1.01 [5] include regular expressions and/or automata, making specication and verication tools that are based on automata even more essential and popular...

    Benjamin Aminofet al. On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Wo...

    • ...Similarly, specication formalisms like ETL [24], which have automata within the logic, involve complementation of automata, and the dicult y of complementing B uchi automata is an obstacle to practical use [1]...

    Ehud Friedgutet al. Büchi Complementation Made Tighter

    • ...Recent industrial-strength property-specica tion languages such as Sugar [4], ForSpec [1], and the recent standard PSL 1.01 [20] include regular expressions and/or automata, making specication and verication tools that are based on automata even more essential and popular...

    Orna Kupferman. Exponential Gapsinour Knowledge

Sort by: