SPICED: Simple PROMELA Interpreter with Crucial Event Detection

 

 

SPICED is an experimental model checking tool that implements the lattice theoretic techniques described in our paper: Producing short counterexamples using Crucial Events. SPICED is based on the SPIN implementation, and uses the same input language, PROMELA, to specify models.

 

Download

The tool, along with all the examples we have run it on, is available here.

SPICED produces error trails in the same format as SPIN. These error trails can be examined using SPIN's guided simulation feature (spin -p).

For now, SPICED only supports UNIX platforms (actually, was only tested on Linux).

You *MUST* gunzip and untar the distribution file in your home directory (wherever ~ redirects to).

 

Experimental Results

 

We ran SPICED on a large collection of PROMELA models from the BEEM database. Many models in the BEEM database contain errors injected into them, and specify the LTL properties to be verified on these models. For SPIN, the LTL properties were specified either in the form of simple assert() statements whenever possible, or as never claims. The "Model" column in the table below contains links to the PROMELA source for each of the models. The "Formula" column contains links to the CETL property specified in SPICED.

 

 

 

SPICED

 

SPIN

Model

Time

States

Transitions

Memory (MB)

Formula

Length of trail

Trail reduction factor

Time

States

Transitions

Memory (MB)

Length of trail

anderson.1

0.014

99

90

3.147

EF(p && EG q)

39

67.56410256

0.018

1317

1320

2.622

2635

anderson.3

0.014

246

287

3.147

EF(p && EG q)

58

51.48275862

0.02

1492

1503

2.622

2986

anderson.5

0.03

6664

12605

3.454

EF(p && EG q)

74

413.8918919

0.125

15312

15792

4.606

30628

anderson.7

0.032

65387

141208

7.038

EF(p && EG q)

82

382.7926829

0.13

15692

16252

6.628

31389

at.1

0.016

16

9

3.147

EF(p && EG q)

8

18.875

0.009

74

81

2.622

151

at.2

0.016

16

9

3.147

EF(p && EG q)

8

18.875

0.01

74

81

2.622

151

at.3

0.018

17

10

3.147

EF(p && EG q)

9

24.88888889

0.01

110

121

2.622

224

at.4

0.018

18

11

3.147

EF(p && EG q)

10

29.7

0.01

146

161

2.622

297

at.5

0.018

18

11

3.147

EF(p && EG q)

10

29.7

0.01

146

161

2.622

297

at.6

0.018

18

11

3.147

EF(p && EG q)

10

29.7

0.01

146

161

2.622

297

at.7

0.019

19

12

3.147

EF(p && EG q)

11

33.63636364

0.01

182

201

2.622

370

bakery.1

0.018

2601

2658

3.249

EF(p && EG q)

510

1.97254902

0.019

2071

4412

2.622

1006

bakery.2

0.012

45

40

3.147

EF(p && EG q)

28

5.714285714

0.009

163

423

2.622

160

bakery.3

0.017

2257

3929

3.249

EF(p && EG q)

55

6.509090909

0.012

179

197

2.622

358

bakery.4

0.013

57

52

3.147

EF(p && EG q)

37

16.48648649

0.034

748

2397

2.622

610

bakery.5

1.226

401575

912557

25.573

EF(p && EG q)

158

8.303797468

0.018

656

701

2.622

1312

bakery.6

0.013

69

64

3.147

EF(p && EG q)

46

18.60869565

0.016

896

3181

2.622

856

bakery.7

5.797

1.74E+06

3.99313e

100.837

EF(p && EG q)

670

2.87761194

0.016

964

1044

2.622

1928

bakery.8

5.982

1.50E+06

4.00E+06

92.849

EF(p && EG q)

77

5.662337662

0.01

218

221

2.622

436

driving_phils.1

0.01

85

74

3.147

EF(p && EG q)

53

1.283018868

0.01

34

34

2.622

68

driving_phils.3

0.012

747

850

3.249

EF(p && EG q)

426

1.863849765

0.01

397

397

2.622

794

driving_phils.4

0.011

212

224

3.147

EF(p && EG q)

123

1.382113821

0.01

85

85

2.622

170

fischer.1

0.013

23

15

3.147

EF(p && EG q)

14

6.071428571

0.008

48

57

2.622

85

fischer.2

0.013

24

16

3.147

EF(p && EG q)

15

15.33333333

0.01

156

224

2.622

230

fischer.3

0.013

26

18

3.147

EF(p && EG q)

17

91.88235294

0.02

1237

2348

2.622

1562

fischer.4

0.014

27

19

3.147

EF(p && EG q)

18

297.8333333

0.05

6454

16351

3.032

5361

fischer.5

0.014

28

20

3.147

EF(p && EG q)

19

268.3684211

0.04

4744

10211

2.929

5099

fischer.6

0.015

28

20

3.147

EF(p && EG q)

19

777.3684211

0.155

21860

62703

5.118

14770

fischer.7

0.015

28

20

3.147

EF(p && EG q)

19

497.3684211

0.07

8016

19323

3.236

9450

frogs.1

0.012

1436

1481

2.724

EF(p)

86

1

0.01

1433

1479

2.622

86

frogs.2

0.036

9859

17191

3.236

EF(p)

30

1

0.03

9856

7333

3.032

30

frogs.3

0.414

190318

191715

16.446

EF(p)

261

1

0.38

190315

191713

13.988

261

gear.1

0.014

1060

2102

2.827

EF(p)

1256

2.265923567

0.027

3186

4144

2.929

2846

gear.2

0.03

4185

7527

3.134

EF(p)

5056

3.836234177

0.133

22386

29769

5.502

19396

lamport.1

0.013

230

352

3.147

EF(p && EG q)

28

10.85714286

0.01

152

168

2.622

304

lamport.2

0.011

92

105

3.147

EF(p && EG q)

14

21.71428571

0.01

152

168

2.622

304

lamport.3

0.011

63

67

3.147

EF(p && EG q)

17

5.411764706

0.01

46

50

2.622

92

lamport.5

0.014

1221

2609

3.147

EF(p && EG q)

29

28.89655172

0.02

419

474

2.622

838

lamport.6

0.012

483

683

3.147

EF(p && EG q)

19

37.05263158

0.01

352

401

2.622

704

lamport.7

0.06

6850

18913

3.454

EF(p && EG q)

30

44.33333333

0.02

665

749

2.622

1330

lamport.8

0.015

1087

2027

3.147

EF(p && EG q)

25

4.32

0.01

54

58

2.622

108

loyd.1

0.009

47

79

2.724

EF(p)

42

1

0.009

363

810

2.622

42

loyd.2

0.194

50931

86545

9.24

EF(p)

52597

1.604996483

0.634

166133

340572

17.611

84418

mcs.1

0.011

345

501

3.147

EF(p && EG q)

12

22.33333333

0.01

133

147

2.622

268

mcs.2

0.011

118

131

3.147

EF(p && EG q)

29

2.482758621

0.01

35

37

2.622

72

mcs.3

0.017

2710

4930

3.249

EF(p && EG q)

13

91.15384615

0.01

591

653

2.622

1185

mcs.4

0.012

771

1148

3.147

EF(p && EG q)

30

2.3

0.01

33

35

2.622

69

mcs.5

0.094

30227

65051

4.888

EF(p && EG q)

14

403.2857143

0.03

2821

3109

2.724

5646

mcs.6

0.032

8871

16010

3.659

EF(p && EG q)

36

2.222222222

0.01

38

40

2.622

80

msmie.2

0.016

83

123

2.724

EF(p)

63

3.396825397

0.01

370

433

2.622

214

needham.1

0.011

21

11

2.724

EF(p && q)

11

3.363636364

0.01

296

408

2.622

37

needham.2

0.012

24

13

2.724

EF(p && q)

13

3.230769231

0.01

1313

1958

2.724

42

needham.3

0.012

27

15

2.724

EF(p && q)

15

3.133333333

0.03

4001

6331

2.929

47

needham.4

0.013

27

15

2.724

EF(p && q)

15

3.466666667

0.04

4003

6333

3.032

52

peterson.1

0.011

592

849

3.147

EF(p && EG q)

46

6.130434783

0.01

141

144

2.622

282

peterson.2

0.01

93

89

3.147

EF(p && EG q)

59

6.508474576

0.01

192

203

2.622

384

peterson.3

0.01

50

46

3.147

EF(p && EG q)

37

8.162162162

0.01

151

162

2.622

302

peterson.4

0.018

3004

5008

3.249

EF(p && EG q)

95

16.16842105

0.02

768

826

2.622

1536

peterson.5

0.011

175

171

3.147

EF(p && EG q)

110

56.2

0.04

3091

3344

2.929

6182

peterson.6

0.011

75

71

3.147

EF(p && EG q)

59

97.28813559

0.03

2870

3098

2.827

5740

peterson.7

0.092

29080

58572

4.888

EF(p && EG q)

159

125.6855346

0.098

9992

11897

9.931

19984

phils.1

0.018

15

11

3.147

EF(p && EG q)

6

4.833333333

0.01

15

18

2.622

29

phils.2

0.011

13

9

3.147

EF(p && EG q)

5

98.8

0.01

969

3236

2.622

494

phils.3

0.011

15

11

3.147

EF(p && EG q)

6

80

0.01

253

353

2.622

480

phils.4

0.011

13

9

3.147

EF(p && EG q)

5

16687.6

0.356

41719

64708

9.086

83438

phils.5

0.011

15

11

3.147

EF(p && EG q)

6

8106.166667

0.212

24319

31584

6.36

48637

phils.6

0.044

15

11

3.147

EF(p && EG q)

6

141948.5

3.826

425846

553093

86.219

851691

phils.7

0.051

13

9

3.147

EF(p && EG q)

5

 

**** Could not complete ******

 

phils.8

0.011

15

11

3.147

EF(p && EG q)

6

275788.8333

7.563

827367

1.07E+06

168.907

1654733

POTS

0.888

153775

197109

21.579

EF((p && q) && EG r)

41

5.390243902

0.38

40161

103804

6.718

221

szymanski.1

0.014

80

110

3.147

EF(p && EG q)

31

17.67741935

0.01

274

297

2.622

548

szymanski.2

0.061

19006

45770

4.069

EF(p && EG q)

25

9.28

0.01

116

121

2.622

232

szymanski.3

0.015

138

249

3.147

EF(p && EG q)

37

197.3513514

0.04

3651

4762

2.827

7302

szymanski.4

4.976

1.20251e

3.63667e

70.424

EF(p && EG q)

28

56.14285714

0.01

786

828

2.622

1572

szymanski.5

0.018

256

592

3.147

EF(p && EG q)

43

1811.534884

0.313

38948

47109

9.188

77896