1

我有一个可以用 Spin 验证的测试 Promela 程序（UI 模型）：

int secrets = 0;
int success = 0;
int fails = 0;
int total = 0;

//variables to control
bool windowLogin = false;
bool windowSecret = false;
bool windowNoSecret = false;

//ltl formulas

ltl secret_to_success_password { [] (secrets<=success)} 
ltl check_total { [] (total == success + fails || total + 1 == success + fails)} 
ltl we_open_nosecret { <> (windowNoSecret) } 
ltl we_open_secret { <> (windowSecret) }
ltl we_open_any { [] <> (windowSecret || windowNoSecret)} 
ltl login_check { <> windowLogin -> <> windowSecret} 
ltl no_secret_nosecret { [] !(windowSecret && windowNoSecret) } 

//channels
chan login=[0] of {short};
chan nonsecret = [0] of {short};
chan secret = [0] of {short};

//main
active proctype MainWindow(){
int buf;
printf("Main started");
do
    //infinite loop
    :: {
    printf("Main: go to Login window");
    login! 1;
    login? buf;
    if 
        :: buf == 1 ->  {//ok
            success++;
            printf("Main: open secret window");
            //"open" secret
            secret ! 1;
            secret ? buf;//и ждем его
        }
        :: buf == 0 ->  {//fail
            fails++;
            printf("Main: open nosecret window");
            //"open" nonsecret
            nonsecret ! 1;
            nonsecret ? buf
        }
    fi
}
od
}

active proctype LoginWindow(){
int buf;
printf("Login started");
do
:: {
    login? buf;
    windowLogin = true;
    if 
        ::true-> { printf("Login fail"); windowLogin = false; login ! 0 }
        ::true-> { printf("Login fail"); windowLogin = false; login ! 0 }
        ::true-> { printf("Login ok!"); windowLogin = false; login ! 1 }//p= 1/3 
    fi
}
od
}

active proctype NonSecretWindow(){
int buf;
printf("Non Secret started");
do
:: {
    nonsecret ? buf;
    printf("Non Secret window opened");
    windowNoSecret = true;
    total++;
    windowNoSecret = false;
    nonsecret ! 1;
    printf("Non Secret window closed");
}
od

}

active proctype SecretWindow(){
int buf;
printf(" Secret started");
do
:: {
    secret ? buf;
    printf("Secret window opened");
    windowSecret = true;
    secrets++;
    total++;
    windowSecret = false;
    secret ! 1;
    printf("Secret window closed");
}
od
}

然后我创建了一个相应的 C 程序（第一步，在主窗口中没有循环）：

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdbool.h>

bool windowLogin = false;
bool windowNoSecret = false;
bool windowSecret = false;

int total = 0;
int secrets = 0;
int success = 0;
int fails = 0;

int LoginWindow();
int NonSecretWindow();
int SecretWindow();


int MainWindow()  {
    //printf("Main started\n");
    {
        //printf("Main: go to Login window\n");
        int r = LoginWindow();
        if (r == 1) {
            //printf("Main: open secret window\n");
            success++;
            SecretWindow();
        } else {
            //printf("Main: open nosecret window\n");
            fails++;
            NonSecretWindow();
        }
    }
return 0;
}


int LoginWindow() {
    //printf("Login started\n");
    windowLogin = true;
    if (rand() %3 ==0) {
//      windowLogin = false;
        return 1;
    } else {
//      windowLogin = false;
        return 0;
    }
    return 0;
}

int NonSecretWindow() {
    //printf("Non Secret started\n");
    //printf("Non Secret window opened\n");

    windowNoSecret = true;
    total++;
    //windowNoSecret = false; --- aorai will controll the variable change only in the end of function
    //printf("Non Secret window closed\n");
    return 0;
}

int SecretWindow() {
    //printf("Secret window opened\n");
    windowSecret = true;
    secrets++;
    total++;
    //windowSecret = false;
    //printf("Secret window closed\n");
    return 0;
}

int main() {

    MainWindow();

    return 0;
}

我想尝试在 Frama-C 和 WP 插件中使用 Aoraï LTL（不想手动创建 .ya）。首先，我创建了一个 .ltl 文件

CALL(main) && _X_ (CALL (MainWindow) && _X_ (CALL (LoginWindow) && _X_ (RETURN (LoginWindow) && 
((_X_ (CALL(NonSecretWindow)))||(_X_ (CALL(SecretWindow)))))))

并且可以获得2个未知目标：

[wp] [Alt-Ergo] Goal typed_MainWindow_call_NonSecretWindow_pre : Unknown (Qed:3ms) (81ms)
[wp] [Alt-Ergo] Goal typed_MainWindow_call_SecretWindow_pre : Unknown (Qed:4ms) (79ms)

我也试过

CALL(main) && _X_ (CALL (MainWindow) && _X_ (CALL (LoginWindow) && _X_ (RETURN (LoginWindow) && 
((_X_ (CALL(NonSecretWindow)||CALL(SecretWindow)))))))

结果相同。这个

CALL(main) && _X_ (CALL (MainWindow) && _X_ (CALL (LoginWindow) && _X_ (RETURN (LoginWindow) && (
(_F_ (CALL(NonSecretWindow)||CALL(SecretWindow)))))))

可以证明，但我相信那个不应该是正确的：

CALL(main) && _X_ (CALL (MainWindow) && _X_ (CALL (LoginWindow) && _X_ (RETURN (LoginWindow) && 
((_F_ (CALL(NonSecretWindow)))))))

但它是正确的（所有目标都被证明了）。此外，我尝试在 Promela 中测试我的 LTL 公式（没有 CALL/RETURN/X）：

_G_ (windowLogin => _F_ (windowSecret || windowNoSecret))

我有很多未经证实的目标，甚至是为了测试

_G_ (total == success + fails || total + 1 == success + fails)

内部错误

[aorai] Welcome to the Aorai plugin
[aorai] failure: Term cannot be transformed into exp.
[kernel] Current source was: test_ltl.c:112
         The full backtrace is:
         Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
         Called from file "src/plugins/aorai/aorai_register.ml", line 385, characters 4-31
...

我使用命令行

rm test_ltl_annot.c
frama-c test_ltl.c -aorai-ltl test_ltl.ltl
frama-c -wp test_ltl_annot.c

Frama-C 版本是 Phosphorus-20170501。

我应该如何使用这个插件来验证我的 LTL 测试程序？

4

0 回答 0