y-taka-23

名古屋モデル検査勉強会 #2

前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。

LTL 式による検査

LTL 式の構文

SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。

y-taka-23

/*
 * Leader Election by Chang-Roberts Algorithm
 */

byte leader = 0;  /* number of leaders */

proctype Node(chan ch_in, ch_out) {
    
    byte tok;
    

y-taka-23

IDENTIFICATION DIVISION.
    PROGRAM-ID. RNPCALC.

DATA DIVISION.
    WORKING-STORAGE SECTION.
        01 STACK-POS PIC 9(2) VALUE 1.
        01 STACK.
            03 STACK-DATA PIC 9(4) OCCURS 10 VALUE 0.
        01 EXPR PIC X(20).
        01 EXPR-POS PIC 9(2).

y-taka-23

IDENTIFICATION DIVISION.
    PROGRAM-ID. FIBONACCI.

DATA DIVISION.
    WORKING-STORAGE SECTION.
        01 ARGUMENT PIC 9(2).
        01 RETURN-VALUE PIC 9(25).
        01 RESULT PIC Z(25).
        01 DP-TABLE.
            03 VALS PIC 9(25) OCCURS 99.

y-taka-23

       IDENTIFICATION DIVISION.
         PROGRAM-ID. DEATH-MARCH-05.
       
       DATA DIVISION.
       WORKING-STORAGE SECTION.
       77  FB-STR   PIC X(153).
       77  CNT      PIC 9(2) VALUE 1.
       77  QUOT     PIC 9(2).
       77  REM-3    PIC 9(1).
       77  REM-5    PIC 9(1).

y-taka-23

/*
 * Resource Sharing Problem (Example for Deadlock)
 */

mtype = { LOCK, UNLOCK };

proctype Client(chan to_res1, to_res2) {
    if
    ::  to_res1 ! LOCK(_pid);
        to_res2 ! LOCK(_pid);

y-taka-23

Parameter A : Type.
Parameter beq_A : A -> A -> bool.

Section Uniq.

Require Import Arith List.

Hypothesis beq_A_true : forall x y : A,
                        beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,

y-taka-23

// **************************************************
//  AWS セキュリティグループのモデル
// **************************************************

// 通信プロトコル
enum Protocol { TCP, UDP, ICMP }

// 通信ポート
sig Port {}

y-taka-23

// ************************************
//   命題論理のシークエント計算のモデル
// ************************************

// 論理式
abstract sig Formula {}

// 原子命題
sig Atom extends Formula {}

y-taka-23

open util/ordering[Time]

sig Time {}

abstract sig Event {
    pre, post : Time,
} {
    post = pre.next
}