capital letters to low, and Turing awards

Ch2-2-SoftwareTheory.tex

@@ -142,11 +142,13 @@
 能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，Platzer等人提出的differential (algebraic) dynamic logic可用于大部分混成系统的建模与自动化推理。
 
 5)面向复杂系统的统计模型检验方法
+
 为了避免穷举复杂系统状态而产生的空间爆炸问题，
 统计模型检验方法通过有限多次的执行对系统进行模拟，并使用假设检验来推断这些样本是否提供满足或违反规范的统计证据。虽然基于仿真的解决方案并不能保证正确的结果，但可以限制发生错误的概率。而且，基于模拟的方法比基于搜索的精确方法使用的计算资源要小得多。
 
 6)面向复杂系统的运行时验证方法
-与基于模型的系统静态验证方法不同，运行时验证方法在系统运行过程中监测系统的异常，避免系统出现故障。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
+
+与基于模型的系统静态验证方法不同，运行时验证方法在系统运行过程中监测系统的异常，避免系统出现难以恢复的故障。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
 
 
 \subsection{新型体系结构和计算平台下的程序理论}