Getafix for concurrent Boolean programs:

Getafix implements reachability within a fixed number of context-switches for concurrent recursive Boolean programs.

  • Model-checking algorithm as formulas:
    Reachability in concurrent programs within k context-switches is expre ssed as a fixed-point formula.
    Here is a sample reachability formula for two threads and four context -switches: 4CStemplate.

    • Experiments on a model of a Windows NT Bluetooth example

    Context
    switches    		 Reach? #nodes in BDD
    representing tuples    		 Time(s)
       
    2 processes: 1 adder and 1 stopper
    (12 local variables and 8 global variables)
    1 No 0.6K 5.4
    2 No 1.5K 5.5
    3 No 5.5k 5.7
    4 No 7.0K 5.8
    5 No 13.3K 6.3
    6 No 23.2K 7.3
        
    3 processes: 1 adder and 2 stoppers
    (18 local variables and 8 global variables)
    1 No 0.7K 5.5
    2 No 2.9K 5.5
    3 Yes 9.9K 5.7
    4 Yes 34.6K 6.8
    5 Yes 115.0K 9.2
    6 Yes 370.5K 17.4
        
    3 processes: 2 adders and 1 stopper
    (18 local variables and 8 global variables)
    1 No 0.7K 5.4
    2 No 2.6K 5.6
    3 No 10.4K 6.0
    4 Yes 41.1K 7.6
    5 Yes 90.9K 9.1
    6 Yes 250.1K 9.1
       
       4 processes: 2 adders and 2 stoppers
    (24 local variables and 8 global variables)
    1 No 0.8K 5.5
    2 No 3.6K 5.6
    3 Yes 15.8K 5.9
    4 Yes 67.8K 7.6
    5 Yes 296.9K 13.0
    6 Yes 1227.4K 57.1

    Contact
    Getafix has been devoloped by Salvatore La Torre, P. Madhusudan, and Gennaro Parlato.