-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
812 lines (529 loc) · 46.3 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<title>Hecoz</title>
<meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=1">
<meta name="description" content="myblog">
<meta property="og:type" content="website">
<meta property="og:title" content="Hecoz">
<meta property="og:url" content="http://yoursite.com/index.html">
<meta property="og:site_name" content="Hecoz">
<meta property="og:description" content="myblog">
<meta property="og:locale" content="zh-CN">
<meta name="twitter:card" content="summary">
<meta name="twitter:title" content="Hecoz">
<meta name="twitter:description" content="myblog">
<link rel="alternate" href="/atom.xml" title="Hecoz" type="application/atom+xml">
<link rel="icon" href="/css/images/mylogo.jpg">
<link rel="apple-touch-icon" href="/css/images/mylogo.jpg">
<link href="//fonts.googleapis.com/css?family=Source+Code+Pro" rel="stylesheet" type="text/css">
<link href="https://fonts.googleapis.com/css?family=Open+Sans|Montserrat:700" rel="stylesheet" type="text/css">
<link href="https://fonts.googleapis.com/css?family=Roboto:400,300,300italic,400italic" rel="stylesheet" type="text/css">
<link href="//cdn.bootcss.com/font-awesome/4.6.3/css/font-awesome.min.css" rel="stylesheet">
<style type="text/css">
@font-face{font-family:futura-pt;src:url(https://use.typekit.net/af/9749f0/00000000000000000001008f/27/l?subset_id=2&fvd=n5) format("woff2");font-weight:500;font-style:normal;}
@font-face{font-family:futura-pt;src:url(https://use.typekit.net/af/90cf9f/000000000000000000010091/27/l?subset_id=2&fvd=n7) format("woff2");font-weight:500;font-style:normal;}
@font-face{font-family:futura-pt;src:url(https://use.typekit.net/af/8a5494/000000000000000000013365/27/l?subset_id=2&fvd=n4) format("woff2");font-weight:lighter;font-style:normal;}
@font-face{font-family:futura-pt;src:url(https://use.typekit.net/af/d337d8/000000000000000000010095/27/l?subset_id=2&fvd=i4) format("woff2");font-weight:400;font-style:italic;}</style>
<link rel="stylesheet" href="/css/style.css">
<script src="/js/jquery-3.1.1.min.js"></script>
<script src="/js/bootstrap.js"></script>
<!-- Bootstrap core CSS -->
<link rel="stylesheet" href="/css/bootstrap.css" >
<link rel="stylesheet" href="/css/home.css" >
<link rel="stylesheet" href="/css/vdonate.css" >
</head>
<body>
<header id="header">
<!-- 背景图模式 -->
<div id="intrologo" class="intro-logo" style="background-position:center; background-repeat:no-repeat; background-image: url(); background-size: auto 100%;">
<!-- Support rolling -->
<section class="awSlider">
<div class="carousel slide carousel-fade " data-ride="carousel">
<!-- Wrapper for slides -->
<div class="carousel-inner">
<div class="item active">
<img id="carousel-img0" src="/css/images/home-bg.jpg">
</div>
<!-- 自适应大图 -->
<script>
var img0 = new Image();
var imageTag0 = document.getElementById("carousel-img0");
img0.src = imageTag0.src;
img0.onload=function(){
if (img0.width / img0.height <= document.body.clientWidth / document.body.clientHeight) {
imageTag0.style.width = document.body.clientWidth + "px";
} else {
imageTag0.style.height = document.body.clientHeight + "px";
imageTag0.style.marginLeft = -(document.body.clientHeight * img0.width / img0.height - document.body.clientWidth) / 2 + "px";
}
};
</script>
<div class="item">
<img id="carousel-img1" src="/css/images/sample.jpg">
</div>
<!-- 自适应大图 -->
<script>
var img1 = new Image();
var imageTag1 = document.getElementById("carousel-img1");
img1.src = imageTag1.src;
img1.onload=function(){
if (img1.width / img1.height <= document.body.clientWidth / document.body.clientHeight) {
imageTag1.style.width = document.body.clientWidth + "px";
} else {
imageTag1.style.height = document.body.clientHeight + "px";
imageTag1.style.marginLeft = -(document.body.clientHeight * img1.width / img1.height - document.body.clientWidth) / 2 + "px";
}
};
</script>
<div class="item">
<img id="carousel-img2" src="https://source.unsplash.com/collection/954550/1920x1080">
</div>
<!-- 自适应大图 -->
<script>
var img2 = new Image();
var imageTag2 = document.getElementById("carousel-img2");
img2.src = imageTag2.src;
img2.onload=function(){
if (img2.width / img2.height <= document.body.clientWidth / document.body.clientHeight) {
imageTag2.style.width = document.body.clientWidth + "px";
} else {
imageTag2.style.height = document.body.clientHeight + "px";
imageTag2.style.marginLeft = -(document.body.clientHeight * img2.width / img2.height - document.body.clientWidth) / 2 + "px";
}
};
</script>
</div>
<!-- Controls -->
<a class="left carousel-control" href=".carousel" role="button" data-slide="prev">
<span class="glyphicon glyphicon-chevron-left" aria-hidden="true"></span>
<span class="sr-only">Geri</span>
</a>
<a class="right carousel-control" href=".carousel" role="button" data-slide="next">
<span class="glyphicon glyphicon-chevron-right" aria-hidden="true"></span>
<span class="sr-only">İleri</span>
</a>
</div>
</section>
<script>
$('section.awSlider .carousel').carousel({
pause: '',
interval: 5000
});
var startImage = $('section.awSlider .item.active > img').attr('src');
$('section.awSlider .carousel').on('slid.bs.carousel', function () {
var bscn = $(this).find('.item.active > img').attr('src');
$('section.awSlider > img').attr('src', bscn);
});
</script>
<canvas width="100%" height="100%"></canvas>
<script>
var c = document.getElementsByTagName('canvas')[0],
x = c.getContext('2d'),
w = window.innerWidth,
h = window.innerHeight,
pr = window.devicePixelRatio || 1,
f = 90,
q,
m = Math,
r = 0,
u = m.PI*2,
v = m.cos,
z = m.random
c.width = w*pr
c.height = h*pr
x.scale(pr, pr)
x.globalAlpha = 0.6
<!-- 折线Polyline背景 -->
</script>
<div id="homelogo" class="homelogo" style="background: rgba(255,255,255,1);">
<div class="homelogoback" style="border: 1px solid #404040;" >
<h1><a href="#content" id="logo">Hecoz</a></h1>
<h3>myblog</h3>
<h5>Hecoz</h5>
<!-- <p><a href="https://github.com/iTimeTraveler" target="_blank">Github</a></p> -->
</div>
</div>
</div>
<!-- 自适应主页背景大图 -->
<!-- home_logo_image居中 -->
<script>
var homelogodiv = document.getElementById("homelogo");
if (document.all.homelogo.offsetWidth > document.body.clientWidth) {
homelogodiv.style.width = document.body.clientWidth + "px";
homelogodiv.style.marginLeft = document.body.clientWidth * -0.5 + "px";
} else {
homelogodiv.style.width = homelogodiv.clientWidth + "px";
homelogodiv.style.marginLeft = (homelogodiv.clientWidth) * -0.5 + "px";
}
</script>
<div class="intro-navigate">
<p class="navigater-list">
<a id="beautifont" class="main-nav-link" href="/">首页</a>
<a id="beautifont" class="main-nav-link" href="/archives">归档</a>
<a id="beautifont" class="main-nav-link" href="/categories">分类</a>
<a id="beautifont" class="main-nav-link" href="/tags">标签</a>
<a id="beautifont" class="main-nav-link" href="/about">关于</a>
</p>
</div>
</header>
<div id="container">
<div id="wrap">
<div id="content" class="outer">
<section id="main" style="float:none;">
<article id="post-005JPF components" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/30/005JPF components/">JPF Application Goals and Types</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/30/005JPF components/" class="article-date">
<time datetime="2017-12-30T13:15:04.000Z" itemprop="datePublished">2017-12-30</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<h3 id="JPF-components"><a href="#JPF-components" class="headerlink" title="JPF components"></a>JPF components</h3><p>  Java™不仅仅是一种编程语言。它是一组层，从特定于平台的VM实现开始 (“host VM”),它位于为您的操作系统编写和使用的本机库之上。在这个结构上，我们添加了JPF — 一个运行在 Host VM上的java应用程序，但是它本身是一个虚拟机用来执行你的被测系统（SUT）。</p>
<p><img src="https://cl.ly/2G3Q0M2v450M/jpf-stack.png" alt="jpf-stack"></p>
<p>  所有这些递归,对于java代码到底是在那个水平进行处理这是容易混淆的。更糟的是，大多书的标准库类文件（java.*classes）和一些注解同时被两个虚拟机运行，当然，在不同的实例。本页的目的是了解代码与系统的不同层和部件相关的一些指示灯。</p>
<p>  为了进一步的说明，我们退一步，看看在将JPF应用在SUT上时使用到了哪些组件。我们从两个方面对组件进行分类：</p>
<blockquote>
<p>processing VM (host VM, JPF)</p>
<p>associated distribution entity 关联分布实体(host Java installation, JPF core, JPF extensions, SUT)</p>
</blockquote>
<p>  还记得what is jpf中的介绍图吗？下面这个图更详细一点：<br><img src="https://cl.ly/1O3M3Y272N40/jpf-components.png" alt="jpf-components"></p>
<p>  让我们从左往右看这幅图，我们从要验证的编译后的java应用程序开始，这当然不是JPF一部分，但是要通过JPF来执行。因此，相应的类文件不必在主机VM中可见（因为运行在JPF上）。但是，应用程序代码可能使用驻留在JPF发行版中的类和接口（例如框架的UML状态图建模，或验证相关的注释类型从JPF APROP扩展）。同时，应用程序和这些建模库和/或注释形成被测试系统(SUT)。</p>
<p>  接下来是JPF核心本身，现在我们知道这是一个用java写的虚拟机，所以你可以运行在任何装有java的系统上。这意味着构成JPF的所有类都必须对“主机jvm”可见。例如，通过设置CLASSPATH环境变量(这不是建议的方法)。</p>
<p>  下面是重要的一部分：<strong>JPF不是一个单一的系统</strong>。它使用各种配置的组件来执行以下任务：</p>
<ul>
<li>property implementation</li>
<li>library modeling</li>
<li>report generation</li>
</ul>
<p>除此之外还有更多，即使你在运行时不指定任何东西，Jpf将使用默认配置，该配置将引入许多组件，如监听器listener。它们不必是JPF核心的一部分，但可以驻留在它们自己的JPF扩展模块中。</p>
<p>如果您确实指定了自己的配置，您可以告诉JPF使用位于JPF核心发行版之外的组件，无论是在已安装的JPF扩展模块中还是在您自己的项目中。无论哪种方式，所有这些 listeners, native peers, publishers和其他组件都处于整个JPF系统的运行时部分，因此它们需要在主机VM中可见。</p>
<p>  最后一部分是最棘手的部分，您的应用程序很可能使用标准java库（e.g. System.out.println()。当jpf执行sut时，一些标准库类必须替换为jpf特定的版本（例如，类如java.lang.classthat有本地方法），不过JPF有一个特殊的MJI机制来实现这一点。然而，大多数标准库类都有纯java实现，我们可以从主机JVM的安装中直接获取这些。</p>
<p>  JPF保持关联的类路径分离。在JPF配置中有三种不同的路径设置：</p>
<ul>
<li><p>native_classpath — 这包括必须对主机vm可见的所有内容，主要包括JPF本身的类，listeners, native peers和bytecode instruction sets。</p>
<blockquote>
<p>The native_classpath is dynamically constructed from your site.properties and jpf.properties configuration files during JPF startup, and processed by the JPF classloader</p>
</blockquote>
</li>
<li><p>classpath — 这包括由JPF执行的类。</p>
</li>
<li>sourcepath — 取决于必须由JPF生成的报告,它可能必须为执行的类文件(字节码)查找SUT和库源。这就是如何告诉JPF这些源位于何处。</li>
</ul>
<p>可以从应用程序属性文件或命令行显式地设置这些路径列表，但是最好让JPF在处理JPF组件的JPF.properties文件时收集它们，这些文件都包括类似的行：</p>
<blockquote>
<p>\<jpf-module>.native_classpath = .. <br><br>\<jpf-module>.classpath = .. <br><br>\<jpf-module>.sourcepath = .. <br></jpf-module></jpf-module></jpf-module></p>
</blockquote>
<p>警告：如果–在启动JPF期间–您会遇到如下消息:</p>
<blockquote>
<p>…<br>[SEVERE} error during VM runtime initialization: wrong model classes (check ‘classpath’)</p>
</blockquote>
<p>这意味着CLASSPATH设置是错误的，jpf加载了一些必须用自己的版本替换的标准库类。they need to be modeled (like java.lang.Thread, java.lang.Class and others - all part of jpf-classes.jar within the jpf-core module).</p>
<p>This can also happen later-on with less essential library classes that are not part of jpf-core, but should be loaded from one of the installed extensions. In this case, this usually shows up as an UnsatisfiedLinkError</p>
</div>
<footer class="article-footer">
<ul class="article-tag-list"><li class="article-tag-list-item"><a class="article-tag-list-link" href="/tags/JPF/">JPF</a></li></ul>
</footer>
</div>
</article>
<!-- Table of Contents -->
<article id="post-004JPF Application Goals and Types" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/30/004JPF Application Goals and Types/">JPF Application Goals and Types</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/30/004JPF Application Goals and Types/" class="article-date">
<time datetime="2017-12-30T12:25:04.000Z" itemprop="datePublished">2017-12-30</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<h3 id="JPF-Application-Goals-and-Types-JPF应用程序目标和类型"><a href="#JPF-Application-Goals-and-Types-JPF应用程序目标和类型" class="headerlink" title="JPF Application Goals and Types JPF应用程序目标和类型"></a>JPF Application Goals and Types JPF应用程序目标和类型</h3><p>  到目前为止，您已经知道在JPF上运行在编译的java程序，就像普通的java虚拟机。但是，使用JPF的目的是什么？而且基于这些目的，不同的JPF应用程序类型是什么。</p>
<h4 id="Why-to-Use-JPF"><a href="#Why-to-Use-JPF" class="headerlink" title="Why to Use JPF?"></a>Why to Use JPF?</h4><p>  在我们对不同类型的jpf应用程序进行分类之前，值得一提的是为什么我们真的想应用它。忠告：如果你有一个严格的顺序程序，只有几个定义良好的输入值，你最好写几个测试用例 – 使用JPF对你的帮助并不会太多。<br><br><strong>使用JPF的两大主要原因有：</strong></p>
<ul>
<li><p><strong>Explore Execution Alternatives 可选择执行方案</strong><br><br>  毕竟，jpf最初是作为软件模型检查器开始的,所以它最初的领域是探索执行的选择,其中我们有四种不同的类型:<br></p>
<ul>
<li>scheduling sequences — 并发应用仍然是JPF应用程序的主要领域，因为(a)死锁和数据竞争等缺陷是微妙的，通常是虚假的。 (b)调度程序通常无法从测试环境中控制。也就是说，这很难甚至不可能被检测。另一方面，JPF不仅“拥有”调度程序（它是虚拟机),而且可以开发所有的调度组合。<font color="red">它甚至可以让你自己定义调度的策略</font>。</li>
<li>input data variation — JPF允许您探索通过启发式定义的输入值集(例如低于、等于或高于某个阈值的值),这在编写测试驱动程序时特别有用。</li>
<li>environment events — 像Swing或Web应用程序之类的程序类型通常会对类似于用户输入的外部事件作出反应，这样的事件可以由JPF作为选择集来模拟。</li>
<li>control flow choices — JPF不仅可以检查程序对具体输入的反应，它还可以回头，系统地探索程序控制结构(分支指令)，以计算将执行代码某一部分的输入数据值。</li>
</ul>
</li>
<li><p><strong>Execution Inspection 执行检查</strong><br><br>  即使你的程序没有很多执行选项，你可以利用JPF的检验能力。作为一台可扩展的虚拟机，实现<font color="pink">coverage analyzers 覆盖分析器</font>或<font color="pink">non-invasive tests 非侵入性测试</font>相对容易，否则会忽略这些情况，因为它们很难或很乏味地实现(比如数字指令中的溢出)。</p>
</li>
</ul>
<h4 id="JPF-Application-Types-JPF应用类型"><a href="#JPF-Application-Types-JPF应用类型" class="headerlink" title="JPF Application Types JPF应用类型"></a>JPF Application Types JPF应用类型</h4><p>  有三种基本的JPF应用类型，它们各有不同的优势和劣势：<strong>JPF- aware</strong>, <strong>unaware</strong> 和 <strong>“enabled” programs</strong>。<br><img src="https://cl.ly/0N0C3l2C2Z21/app-types.png" alt="app-types"></p>
<p><strong>JPF unaware programs</strong><br>这是通常的情况 — 在应用程序中运行jpf，该应用程序通常不知道验证。它只在任何兼容java的vm上运行。使用JPF检查这种应用的典型原因是查找难以测试的所谓的违反非函数属性，例如死锁或竞争条件。JPF特别擅长发现和解释与并发相关的缺陷，但你得知道代价：JPF比java虚拟机慢得多（它比正常的字节代码解释器做的更多），它可能不支持受测试系统使用的所有Java库。</p>
<p><strong>JPF dependent programs</strong><br>我们有模型的应用程序 — 他们存在唯一目的是验证通过JPF(例如，检查某个算法)，所以java恰好是实现语言因为这是JPF的理解。通常，这些应用程序是基于特定于域的框架(例如状态扩展？)编写的，以便JPF能够验证模型。因此，模型应用程序本身通常较小，规模很好，并且不需要额外的特性规范。缺点是开发底层域框架非常昂贵。</p>
<p><strong>JPF enabled programs</strong><br>第三类的投资回报可能是最好的，可以在任何VM上运行的程序，但是包含表示无法用标准Java语言表示的属性的java注释。</p>
<blockquote>
<p>For example, assume you have a class which instances are not thread safe, and hence are not supposed to be used as shared objects. You can just run JPF and see if it finds a defect (like a data race) which is caused by illegally using such an object in a multi-threaded context. But even if JPF out-of-the-box can handle the size of the state space and finds the defect, you probably still have to spend a significant effort to analyze a long trace to find the original cause (which might not even be visible in the program). It is not only more easy on the tool (means faster), but also better for understanding if you simply mark the non-threadsafe class with a @NonShared annotation. Now JPF only has to execute up to the point where the offending object reference escapes the creating thread, and can report an error that immediately shows you where and how to fix it.</p>
<p>There is an abundance of potential property-related annotations (such as @NonNull for a static analyzer and JPF), including support for more sophisticated, embedded languages to express pre- and post-conditions.</p>
</blockquote>
</div>
<footer class="article-footer">
<ul class="article-tag-list"><li class="article-tag-list-item"><a class="article-tag-list-link" href="/tags/JPF/">JPF</a></li></ul>
</footer>
</div>
</article>
<!-- Table of Contents -->
<article id="post-003JPF Features and Classification" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/30/003JPF Features and Classification/">JPF Features and Classification</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/30/003JPF Features and Classification/" class="article-date">
<time datetime="2017-12-30T11:29:04.000Z" itemprop="datePublished">2017-12-30</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<h3 id="JPF-Features-and-Classification"><a href="#JPF-Features-and-Classification" class="headerlink" title="JPF Features and Classification"></a>JPF Features and Classification</h3><p>  到目前为止，应该清楚的是，JPF不仅仅是一个模型检查器：它是一个可以用于模型检查的JVM。但是，如果您熟悉正式的方法，您可能想知道支持什么样的模型检查方法和特性。</p>
<p>一些基本的模型检查特性是：</p>
<p><strong>Explicit State 显示状态</strong> 模型检查是JPF的标准操作模式，这意味着JPF跟踪局部变量的具体值，栈，堆对象和线程状态。不包括故意的不同的调度行为之外。JPF应该产生相同的结果，像一个正常的JVM。当然它比较慢（它是在JVM上运行的JVM，做了很多额外的工作）。</p>
<p><strong>Symbolic Execution 符号执行</strong> 意味JPF可以执行从当前执行路径中使用某个变量获得的符号值来执行程序。</p>
<blockquote>
<p>Symbolic Execution means that JPF can perform program execution with symbolic values obtained from how a certain variable was used along the current path of execution (e.g. “x > 0 && x < 43”).</p>
</blockquote>
<p>此外，JPF甚至可以混合具体和符号执行，或者在他们之间切换。有关详细信息，请参阅Symbolic Pathfinder project文档。</p>
<p><strong>State Matching 状态匹配</strong> 状态匹配是避免不必要工作的关键机制，程序的执行状态主要由堆和线程堆栈快照组成。而JPF执行，它检查每个新的状态是否已经看到一个相等的状态，在这种情况下，沿着当前的执行路径继续下去是没有用的，而且JPF可以回到最近的未探索的非确定性选择。哪些变量有助于状态匹配，并且可以由用户控制状态匹配。</p>
<p><strong>Backtracking 回溯</strong> 回溯意味着jpf可以恢复以前的执行状态，看看是否还有未执行的选择。例如，如果JPF达到程序结束状态，它会回退以寻找不同的尚未执行的调度序列。理论上，这可以通过从一开始就重新执行程序来实现，如果优化了状态存储，回溯是一种更有效的机制。</p>
<p><strong>Partial Order Reduction 偏序约简</strong> 偏序是JPF采用减少上下文切换线程之间不产生有趣的新程序状态，这是即时完成的，即不预先分析或注释程序，通过检查哪些指令可以产生线程间的影响。虽然这是快速的，但它不能处理“diamond case”（应该翻译成极少见的例子），因为它不能在当前执行之前看到。</p>
<p>JPF的灵活性是通过提供大量扩展点的体系结构来实现的，其中最重要的是：<br></p>
<ul>
<li>search strategies 搜索策略 – 控制搜索状态空间的顺序</li>
<li>listeners 监听器 – 监视JPF的执行并与之交互(例如检查新属性)</li>
<li>native peers 本地同行 – to model libraries and execute code at the host VM level</li>
<li>bytecode factories – 提供不同的执行模型(如符号执行)</li>
<li>publishers – 生成特定的报告</li>
</ul>
<p>通常，通过配置的灵活性是JPF对软件模型检查的可扩展性问题的回答。</p>
</div>
<footer class="article-footer">
<ul class="article-tag-list"><li class="article-tag-list-item"><a class="article-tag-list-link" href="/tags/JPF/">JPF</a></li></ul>
</footer>
</div>
</article>
<!-- Table of Contents -->
<article id="post-002Testing vs. Model Checking" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/30/002Testing vs. Model Checking/">Testing vs. Model Checking</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/30/002Testing vs. Model Checking/" class="article-date">
<time datetime="2017-12-30T08:39:04.000Z" itemprop="datePublished">2017-12-30</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<h3 id="Testing-vs-Model-Checking"><a href="#Testing-vs-Model-Checking" class="headerlink" title="Testing vs. Model Checking"></a>Testing vs. Model Checking</h3><p>  那么JPF所做的是测试我们的程序是否存在缺陷？不，它通常做得更多，至少当用作模型检查器时。那么，测试与模型检查有什么不同？</p>
<p>  软件测试是一组经验技术，您可以在程序中执行大量输入，以确定其行为是否正确。这包括两个部分，它们涉及到正确的选择：<strong>test input and test oracle</strong>。</p>
<p><img src="https://cl.ly/2i3Y0n340I2N/states-testing.png" alt="states-testing"></p>
<p>  Testing 测试技术在我们如何选择输入时有所不同(random, “interesting” problem domain values like corner cases etc)，以及对于被测系统的了解情况（system under test SUT），以及它的执行环境（黑/灰/白盒），这尤其影响我们如何定义和检查正确的行为。这需要大量的猜测，或者像Edsger dijkstra所说的：“程序测试最多只能显示错误的存在，但绝不能显示错误的缺失”，为此，我们通常通过执行“足够多”的测试用例来实现这一点。测试复杂系统通常可以说是大海捞针。如果你是一个优秀的测试人员，你做出了正确的猜测，并击中不可避免的缺陷。如果不是，不要担心-你的用户稍后会发现它。</p>
<p><img src="https://cl.ly/012S0q2a3j2E/states-testing.png" alt=""></p>
<p>  Model Checking 模型检验作为一种非形式化方法，不依赖于猜测。至少理论上是这样的，如果有违反给定规范的行为,模型检查会找到的。模型检验被认为是一种严格的方法，它详尽地探索了SUT所有可能的行为。</p>
<p>  为了说明这一点,请看例子<a href="https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/random_example" target="_blank" rel="noopener">Random number example</a> 这显示了如果我们有一个使用随机值序列的程序，测试与模型检查是不同的:测试每次只处理一组值,而且我们对每一组没有控制权。而模型检查在检查所有数据组合或发现错误之前是不会停止的。</p>
<p>  用Random number example这个例子，我们至少可以看到程序中的选择。假设这是一个并发编程示例<a href="https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/race_example" target="_blank" rel="noopener">concurrent programming example</a>，您知道操作系统在线程之间切换的位置吗？我们所知道的是不同的调度序列可能导致不同的程序行为（如过有数据竞争的话）。但是我们在测试中很难强制改变调度的行为。有程序/测试规格的组合，是“不可测”。但是作为一台虚拟机，我们的软件模型检查器不会遭受相同的命运-它完全控制我们程序的所有线程，而且可以执行所有的调度组合。</p>
<p>  这只是理论，实际上，“all possible”可能是一个相当大的数字-对于现有的计算资源或我们的耐心来说太大了。假设一个程序不同的调度序列有N个线程组成（P1…Pn），每个都有n<sub>i</sub>原子指令序列。</p>
<p><img src="https://cl.ly/1L463I2M2Z0u/intervings.png" alt="intervings"></p>
<p>  对于拥有2个原子片段的两个线程来说，每一个都给了我们6种不同的调度组合。对于有8个原子片段来说，这个数字是12870，有16个片段的是601080390-这就是为什么它容易产生状态爆炸。软件模型检查具有可测量性问题，甚至比硬件的模型检查更重要，因为程序通常有更多的状态。</p>
<blockquote>
<p>  There are several things we can do. First, we can optimize the model checker, which is simply an engineering feat. Next, we can find program states which are equivalent with respect to the properties we are checking, which can be done with various degrees of abstractions and value representations. Last, we can try to get to the defect first, before we run out of time or memory. But this is where the boundary between testing and model checking becomes blurred, as it involves things like heuristics about interesting input values or system behaviors, and these heuristics tend to drop reachable program states.</p>
</blockquote>
<p>  我们可以做这样几件事。首先，我们可以优化模型检查器，这将是一个工程壮举。接下来，我们可以找到与我们正在检查的属性等价的程序状态，可以用不同程度的抽象和价值表示来完成。最后，我们可以尝试在再耗尽时间或内存之前先找到缺陷。但是这就是测试和模型检查之间的界限变得模糊的地方，因为它涉及到诸如关于有趣的输入值或系统行为的启发式方法，而这些启发式方法倾向于删除可访问的程序状态。</p>
<p>  JPF做了这些来限制状态爆炸的发生。而且大多数东西都是配置的，而不是硬连接的。所以你不依赖于内置的启发式方法。但不管我们缩小了多少状态空间，与常规测试相比，JPF仍然可以观察到更多关于程序执行的信息，而且它仍然知道执行的历史，以防我们发现一个缺陷–这只是第一部分。我们还需要理解它，使它最终可以被解决。</p>
</div>
<footer class="article-footer">
<ul class="article-tag-list"><li class="article-tag-list-item"><a class="article-tag-list-link" href="/tags/JPF/">JPF</a></li></ul>
</footer>
</div>
</article>
<!-- Table of Contents -->
<article id="post-001what is jpf" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/30/001what is jpf/">what is jpf？</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/30/001what is jpf/" class="article-date">
<time datetime="2017-12-30T08:29:04.000Z" itemprop="datePublished">2017-12-30</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<h3 id="What-is-JPF"><a href="#What-is-JPF" class="headerlink" title="What is JPF?"></a><strong>What is JPF?</strong></h3><p>  JPF 的功能取决于你如何去配置它，首先，没有一个单一的JPF，它是运行时配置的不同组件的组合。JPF的设计使其易于扩展。因此，我们在此仅限于说明<em>jpf core</em>是什么，但是请记住这只是jpf组建中最主要的一部分而已。</p>
<h4 id="The-Core-a-VM-that-supports-Model-Checking-（核心：支持模型检查的VM）"><a href="#The-Core-a-VM-that-supports-Model-Checking-（核心：支持模型检查的VM）" class="headerlink" title="The Core : a VM that supports Model Checking （核心：支持模型检查的VM）"></a>The Core : a VM that supports Model Checking <strong>（核心：支持模型检查的VM）</strong></h4><p>  JPF内核是用于解释Java™字节码的虚拟机(VM)，这意味着它是一个可以执行java程序的程序。它用于查找这些程序中的缺陷，因此您还需要提供属性来作为输入检查。</p>
<p><img src="https://cl.ly/0I22290V3f1G/jpf-basic.png" alt="JPF"></p>
<p>  JDF基于java实现，所以不要期望他可以有java虚拟机一样运行速度。他是一个运行在java虚拟机上的虚拟机。java的语法已经定义在<a href="http://java.sun.com/docs/books/jvms/second_edition/html/VMSpecTOC.doc.html/" target="_blank" rel="noopener">Sun’s Java Virtual Machine Specification</a>中，我们在JPF中几乎没有固定的语义-VM指令集由一组可替换的类表示。</p>
<p>  JPF使用下面的特征来设定默认的指令集：<em>execution choices（执行选项）</em> JPF可以从不同的执行过程中识别出程序中的点，然后系统地探索所有这些点。这意味着JPF(理论上)通过程序执行所有路径，不像普通的java虚拟机。特定的选择是不同的调度序列或随机值。但是，JPF允许您介绍您自己的选择，如用户输入或状态事件。</p>
<p>  路径的数量可能会失控，而且它通常会。这就是软件模型检查所称的 <strong>状态爆炸问题(state explosion problem)</strong>。所以JPF采用的第一套办法就是 <strong>状态匹配(state matching)</strong><br>每当JPF到达一个选择点，都会检查是否已经有了相似的程序状态，在这种情况下，它可以安全地放弃这条执行序列，回溯到以前的尚未被探索的选择点，然后从那里出发。没错，JPF可以恢复程序状态，这就像告诉调试器“回溯100个指令”一样。</p>
<p>  那么这些特性是用来做什么的呢？通常是要在程序中找到要验证的缺陷，是什么样的缺陷呢？现在你应该知道答案了：这取决于你如何配置JPF。JPF-core 检测可以有VM检测出的缺陷，并且不需要你指定任何缺陷属性：<strong>死锁和未处理的异常（包括java assert 表达式）</strong> ，我们称这些为非函数特性，任何应用程序都不应违反它们。但是JPF并不仅仅限于此–您可以定义您自己的属性，通常用 <strong>listener</strong> 来完成，一个可以让您密切监视JPF所采取的所有操作的“小插件”，比如执行单个指令，创建对象，达到一个新的程序状态等等。这样一个典型的listener实现的本质是一个竞争检测器，它标识并发程序中对共享变量的不同步访问(JPF核心包括其中的两个)。</p>
<p>  另外一个有用的特性是，如果JPF发现了缺陷JPF可以获得导致错误的完整执行历史的记录，如果您需要的话，可以执行每个执行的字节码指令。我们称之为 <strong>程序跟踪（trace）</strong> ，发现缺陷的真正原因是无价的。拿死锁来说——通常没有多少可以直接从调用堆栈快照中推断出来。</p>
<p>  所有的这些解释了为什么JPF被称为 <strong>开挂的调试工具箱（a debugger toolbox on steroids）</strong>首先，它会以所有可能的方式自动执行程序，以找到甚至您还不知道的缺陷，然后它解释了你造成这些缺陷的原因。</p>
<h4 id="Caveat-not-a-lightweight-tool-（警告：不是一个轻量级的工具）"><a href="#Caveat-not-a-lightweight-tool-（警告：不是一个轻量级的工具）" class="headerlink" title="Caveat : not a lightweight tool （警告：不是一个轻量级的工具）"></a>Caveat : not a lightweight tool （警告：不是一个轻量级的工具）</h4><p>  当然，那是理想的状态。实际上，这可能需要相当多的配置，甚至需要一些编程。jpf不是像编译器那样的“黑盒（black box）”工具，学习曲线可能很陡峭。更糟的是JPF不能执行利用本地代码的java库。不是因为它不知道怎么做，而是因为这样做通常没有意义：本机代码类似于系统调用来写入文件不易恢复-JPF将失去其匹配或回溯程序状态的能力。当然还有有补救办法，而且是可配置的：<em>native peers</em> 和 <em>model classes</em> 。native peers 是具有用来代替真实本地方法的方法的类。这个代码是由真正的java虚拟机执行，不是JPF，因此，它可以提升运行速度。model classes 是标准类的简单替换，像 <font color="gray" size="3">java.lang.Thread</font>这为完全可观察和可回溯的本机方法提供了可选方案。</p>
<p>  如果您熟悉java实现，你知道的包含库的巨大的比例，很明显，我们不能处理所有这些问题，至少现在不能。没有理论上的限制，实现缺失的库方法通常是非常容易的。但是你应该准备好面对<font color="red" size="3">UnsatisfiedLinkErrors</font>比如你让JPF运行大的生产系统。臭名昭著的白点是 <strong>java.io</strong> 和 <strong>java.net</strong> ，但也有人在做这方面的工作。谁知道呢，也许你也有兴趣加入这项工作-JPF是开源的，没有什么是你不可以看到的。我们现在有二十多个行业的主要合作者，世界各国政府和学术界。</p>
<p>  那么，是什么使投资jpf值得呢？毕竟，它是一个重量级的工具。不是一个快速简单的bug查找器。首先，如果你正在寻找一个研究平台来尝试你的新软件验证思想，chances are you can get along with JPF in a fraction of time compared to native production VMs，它们通常是针对速度而优化的，很少考虑可扩展性或可观察性。<br>第二个答案是，如这篇文章所写的，有些bug只有JPF才能找到(before the fact,that is)，而且还有越来越多的Java应用程序无法在事实之后了解这些错误。JPF是一个针对关键应用的程序，在这些程序中，失败是不能容忍的。这也就不奇怪，JPF是由美国宇航局发起的。</p>
</div>
<footer class="article-footer">
<ul class="article-tag-list"><li class="article-tag-list-item"><a class="article-tag-list-link" href="/tags/JPF/">JPF</a></li></ul>
</footer>
</div>
</article>
<!-- Table of Contents -->
<article id="post-hello-world" class="article article-type-post" itemscope itemprop="blogPost" >
<div id="articleInner" class="article-inner">
<header class="article-header">
<h1 class="thumb" itemprop="name">
<a class="article-title" href="/2017/12/10/hello-world/">Hello World</a>
</h1>
</header>
<div class="article-meta">
<a href="/2017/12/10/hello-world/" class="article-date">
<time datetime="2017-12-10T11:29:04.000Z" itemprop="datePublished">2017-12-10</time>
</a>
</div>
<div class="article-entry" itemprop="articleBody">
<p>Welcome to Myblog</p>
</div>
<footer class="article-footer">
</footer>
</div>
</article>
<!-- Table of Contents -->
</section>
</div>
<div align="center" style="margin-top: 30px;"><hr class="hr" style="margin:0px; height:3px;"></div>
<footer id="footer">
<div class="container">
<div class="row">
<p> Powered by <a href="http://hexo.io/" target="_blank">Hexo</a> and <a href="https://github.com/iTimeTraveler/hexo-theme-hiker" target="_blank">Hexo-theme-hiker</a> </p>
<p id="copyRightEn">Copyright © 2013 - 2017 Hecoz All Rights Reserved.</p>
<p class="busuanzi_uv">
访客数 : <span id="busuanzi_value_site_uv"></span> |
访问量 : <span id="busuanzi_value_site_pv"></span>
</p>
</div>
</div>
</footer>
<!-- min height -->
<script>
var wrapdiv = document.getElementById("wrap");
var contentdiv = document.getElementById("content");
var allheader = document.getElementById("allheader");
wrapdiv.style.minHeight = document.body.offsetHeight + "px";
if (allheader != null) {
contentdiv.style.minHeight = document.body.offsetHeight - allheader.offsetHeight - document.getElementById("footer").offsetHeight + "px";
} else {
contentdiv.style.minHeight = document.body.offsetHeight - document.getElementById("footer").offsetHeight + "px";
}
</script>
</div>
<!-- <nav id="mobile-nav">
<a href="/" class="mobile-nav-link">Home</a>
<a href="/archives" class="mobile-nav-link">Archives</a>
<a href="/categories" class="mobile-nav-link">Categories</a>
<a href="/tags" class="mobile-nav-link">Tags</a>
<a href="/about" class="mobile-nav-link">About</a>
</nav> -->
<!-- mathjax config similar to math.stackexchange -->
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
inlineMath: [ ['$','$'], ["\\(","\\)"] ],
processEscapes: true
}
});
</script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
skipTags: ['script', 'noscript', 'style', 'textarea', 'pre', 'code']
}
});
</script>
<script type="text/x-mathjax-config">
MathJax.Hub.Queue(function() {
var all = MathJax.Hub.getAllJax(), i;
for(i=0; i < all.length; i += 1) {
all[i].SourceElement().parentNode.className += ' has-jax';
}
});
</script>
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
</script>
<link rel="stylesheet" href="/fancybox/jquery.fancybox.css">
<script src="/fancybox/jquery.fancybox.pack.js"></script>
<script src="/js/scripts.js"></script>
<script src="/js/home.js"></script>
<div style="display: none;">
<script src="https://s95.cnzz.com/z_stat.php?id=1260716016&web_id=1260716016" language="JavaScript"></script>
</div>
<script async src="//dn-lbstatics.qbox.me/busuanzi/2.3/busuanzi.pure.mini.js">
</script>
</div>
<div class="modal fade" id="myModal" tabindex="-1" role="dialog" aria-labelledby="myModalLabel" aria-hidden="true" style="display: none;">
<div class="modal-dialog">
<div class="modal-content">
<div class="modal-header">
<h2 class="modal-title" id="myModalLabel">设置</h2>
</div>
<hr style="margin-top:0px; margin-bottom:0px; width:80%; border-top: 3px solid #000;">
<hr style="margin-top:2px; margin-bottom:0px; width:80%; border-top: 1px solid #000;">
<div class="modal-body">
<div style="margin:6px;">
<a data-toggle="collapse" data-parent="#accordion" href="#collapseOne" onclick="javascript:setFontSize();" aria-expanded="true" aria-controls="collapseOne">
正文字号大小
</a>
</div>
<div id="collapseOne" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingOne">
<div class="panel-body">
您已调整页面字体大小
</div>
</div>
<div style="margin:6px;">
<a data-toggle="collapse" data-parent="#accordion" href="#collapseTwo" onclick="javascript:setBackground();" aria-expanded="true" aria-controls="collapseTwo">
夜间护眼模式
</a>
</div>
<div id="collapseTwo" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingTwo">
<div class="panel-body">
夜间模式已经开启，再次单击按钮即可关闭
</div>
</div>
<div>
<a data-toggle="collapse" data-parent="#accordion" href="#collapseThree" aria-expanded="true" aria-controls="collapseThree"> 关 于 </a>
</div>
<div id="collapseThree" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingThree">
<div class="panel-body">
Hecoz
</div>
<div class="panel-body">
Copyright © 2017 Hecoz All Rights Reserved.
</div>
</div>
</div>
<hr style="margin-top:0px; margin-bottom:0px; width:80%; border-top: 1px solid #000;">
<hr style="margin-top:2px; margin-bottom:0px; width:80%; border-top: 3px solid #000;">
<div class="modal-footer">
<button type="button" class="close" data-dismiss="modal" aria-label="Close"><span aria-hidden="true">×</span></button>
</div>
</div>
</div>
</div>
<a id="rocket" href="#top" class=""></a>
<script type="text/javascript" src="/js/totop.js?v=1.0.0" async=""></script>
</body>
</html>