194 lines
37 KiB
TeX
194 lines
37 KiB
TeX
% !TEX root = main.tex
|
||
|
||
任何一个学科的发展都需要基础理论作为支撑。涵盖计算理论与程序理论的软件理论是软件学科的基础。重要的理论结果和方法也有助于实际软件开发。信息技术的快速发展推动了整个社会的信息化程度不断提高。软件作为重要的基础设施之一，需要不断提高其品质。著名软件工程师Laurence Peter Deutsch \cite{Deutsch99}给学生的建议包括：“Good software requires the ability to think formally (mathematically),…Make sure you have some exposure to assertions, proofs, and analysis of algorithms, …”，也就是说，高质量的软件需要进行一定的形式化（数学）分析，确保算法的正确性。
|
||
|
||
|
||
在满足实际需求的过程中，理论本身不断完善。随着软件应用需求和场景的持续发展和丰富、软件运行环境和硬件平台的不断变革、以及软件基础性地位的日益提升，软件理论有着更为广阔的应用前景和发展机遇，但同时也面临巨大的挑战。最近十余年，物联网\index{物联网}、大数据、人工智能等信息领域技术浪潮不断兴起，对计算和程序理论提出了一系列新的需求和挑战。
|
||
|
||
|
||
首先，新型的软件应用需求和场景为软件理论带来挑战。大数据应用需要新型算法和复杂性理论\index{复杂性理论}支持海量数据的高效处理；云计算的发展需要新型的分布式计算理论\index{计算理论}以及新型的编程模型；人工智能的发展使得具有不确定性的知识表示和推理成为一种常规的思维方式，从而为算法和复杂性理论、编程模型、以及软件的可靠性分析\index{软件可靠性}等带来众多问题；信息物理融合系统（CPS）\index{信息物理融合系统}和物联网应用则使得既有离散事件又有连续状态变化的混成系统系统\index{混成系统系统}的建模、分析和验证成为难以回避的挑战。
|
||
|
||
|
||
其次，软件运行环境和硬件平台的变革为软件理论带来机遇和挑战。一方面，处理器能力和网络带宽的大幅提升，使得以往受限于计算或通信能力的技术变得更具有实用性，包括特定的编程模型以及程序的自动化分析和验证技术，从而为软件理论的发展带来新的驱动力。另一方面，运行环境和硬件平台的变革也带来巨大挑战：人、机、物的融合使得软件运行在具有高度动态化和不确定性的环境中，为软件的规约、建模、分析和验证带来困难；多核处理器的普及促进了并发程序的使用，但对于高效并发算法的验证缺少理论和工具支持；其他挑战还包括搭载异构芯片的处理器、云平台上数据一致性的形式化规约和验证等。
|
||
|
||
|
||
其三，软件基础性地位的提升为软件理论带来挑战。软件作为基础设施，日益深入到我们生产生活的方方面面，相应地，对软件可靠性的要求也变得越来越强。人们开始期望那些在以往仅仅针对特定算法和协议的验证技术能够应用于代码级的完整系统验证上，特别是底层系统软件的验证，如操作系统内核、编译器\index{编译器}、密码算法和协议实现等。信息物理融合系统\index{信息物理融合系统}以及基于学习的人工智能技术在自动驾驶等安全攸关系统中的应用使得混成系统和概率系统的形式验证需求越发迫切。同时，软件复杂度的提高，对于可信软件的自动化开发和验证技术也提出了更高的要求。
|
||
|
||
|
||
本章将针对软件理论的核心内容，包括算法及复杂性理论、程序正确性理论等，逐一探讨其面临的挑战，以及将来需要开展的研究。
|
||
|
||
|
||
\section{重大挑战问题}
|
||
在新的时代背景下，特别是在人机物融合的大环境下，软件理论遇到了新的挑战。具体包括：如何应对大规模的数据与计算(§\ref{sec:st-complexity})；如何保证复杂软件系统的正确性、可靠性、安全性(§\ref{sec:st-reliability})；针对新型计算机的硬件架构与新的计算平台，如何建立其理论分析基础(§\ref{sec:st-architecture})。
|
||
|
||
|
||
\subsection{面向数据科学的算法与计算复杂性理论}\label{sec:st-complexity}
|
||
构建高效的软件系统，需要发展算法设计与分析技术；确保算法的性能、理解计算的本质与界限，需要发展相应的计算复杂性理论。算法与计算复杂性理论，就是在这一背景与宗旨下发展形成的，是软件科学乃至计算机科学的根基。随着现代计算机科学进入大数据时代，建立在多项式时间图灵机和最坏情况复杂度分析基础上的传统算法与计算复杂性理论，在计算模型、问题模型和解决标准上，都面临新的挑战。
|
||
|
||
在计算模型方面，面向大规模的实时动态输入数据，多项式时间图灵机这一传统计算模型已难以用来刻画高效计算。面向大数据的计算，往往需考虑并行、分布式、低通信、在线计算、动态输入、局部计算等多种计算模型上的约束。因此需面向这些约束，建立新的计算模型。并在新模型上系统地发展相应的算法设计与分析的新范式，以及包含复杂性下界与分类在内的新的计算复杂性理论。
|
||
|
||
在问题模型方面，随着数据科学的发展，计算的重心逐步由判定、求解、组合优化等关注单个解的传统计算问题转移到推断、学习、统计、采样、度量等关注整个解空间宏观特性的以数据科学为导向的新型计算问题。为这些非传统计算问题提供高效算法，需要发展新的算法设计与分析技术；理解其计算复杂性的变化规律，需要发展“计算相变”等计算复杂性理论。
|
||
|
||
在解决标准方面，面向大数据的计算很多情况下是针对特定分布的真实数据，且往往可以容忍各种形式的近似，因此基于最坏情况复杂度分析的传统已不再适用，需发展数据依赖的算法设计和参数复杂性等非最坏情况复杂性分析，并允许随机与近似计算。另一方面，大数据计算对计算的开销的限制却更加苛刻，因此需发展亚线性时间开销算法、以及精细计算复杂性理论。同时，现实大数据的计算场景还需顾及到隐私、公平、容错等额外的约束，对何为一个计算问题的“解决”有更加丰富的要求。这都需要发展相应的算法设计与分析技术以及计算复杂性理论。
|
||
在实际的软件系统中，上述挑战往往并非单独出现，而是以多种组合形式出现的。因此，不同于算法与计算复杂性理论中很多情况下“一题一议”的特点，需要更加注重发展通用算法技术，研究基本算法原语及其复杂性。发展适应大数据时代的更加“鲁棒”的算法与计算复杂性理论。
|
||
|
||
|
||
\subsection{复杂系统的可靠性保证}\label{sec:st-reliability}
|
||
近年来，计算机越来越深入到人们生活中的方方面面，对软件系统可靠性的要求越来越高。另一方面，随着处理器计算能力的增强和形式验证理论与技术的发展，软件验证的能力也在提高。因此，用形式化验证技术来确保复杂系统的可靠性成为一种可行的方案，得到了越来越多的关注和研究，近年来也出现了一些有代表性的优秀成果。
|
||
|
||
|
||
然而，在软件日益得到广泛应用的同时，其复杂度也在不断增加。软件系统的复杂性主要体现在单点技术特性复杂、系统结构复杂、系统规模庞大等方面。复杂软件系统的验证技术也随之面临重要挑战。在形式化方法中，系统的可靠性或其他安全攸关性质可以通过规约描述，而系统是否满足规约的分析过程依赖于系统的形式化建模、分析和验证。
|
||
|
||
|
||
复杂系统的可靠性挑战主要体现在以下几个方面：
|
||
|
||
|
||
首先，如何准确表示复杂系统的规约。系统的规约一般通过逻辑公式、集合论等来描述对系统安全性、可靠性、正确性等各方面的需求。系统规约要解决的主要问题是，将各种非形式化表述中使用的关键概念和性质，采用简洁直观又容易被用来推理验证的数学和逻辑语言进行描述。
|
||
|
||
|
||
随着系统复杂性的增加和系统应用场景的多样化，使得需要描述的性质变得更加复杂。例如，信息物理融合系统除了关心功能正确性，还关心非功能相关的性质，包括实时、空间位置等时空特性；机器学习算法和系统的正确性和安全性的研究目前仍处于起步阶段，即便非形式的定义和刻画这些性质仍然是开放性问题，其中一些已经被大家所接受的重要性质，如鲁棒性（Robustness），其性质刻画与经典的程序功能正确性刻画显著不同。在并发系统中，除了线性一致性（Linearizability）这种经典的对并发对象的功能正确性的刻画以外，人们还提出了各种新型的量化松弛算法，它们部分放松了线性一致性的要求，但仍然能够提供一定的正确性保证。这些放松后的保证该如何进行形式化的刻画，是目前面临的关键挑战。与之类似，为了解决云计算中分布式多拷贝数据的一致性问题，并在一致性、可用性、以及系统性能方面取得平衡，人们提出了各种不同强度的数据一致性，包括最终一致性、因果一致性、顺序一致性以及各种变体，还包括多种数据一致性相结合的算法和系统，这些不同的一致性的形式化规约是当前研究的热点问题。在信息安全领域，很多安全特性不是描述程序一次运行的性质，而是要刻画程序多次运行之间的关系，如信息流安全中经典的非干扰性（Non-interference），这一类性质往往被称为“超安全性质”（Hyper-properties），其规约也和经典的功能正确性有所不同。
|
||
|
||
|
||
其次，如何形式化表示复杂软件系统。安全攸关领域的很多系统往往可看成是信息物理融合系统在复杂环境中的运行，不仅兼有离散事件与连续的状态变化，同时计算与控制过程共存。由于系统的非确定性，或克服复杂性而进行的简化，很多都具有概率与随机行为。例如，由于风对飞行器运动的影响，网络控制的系统中消息的丢失及其他随机事件。因此，对随机混成系统的建模、分析与验证是非常困难的。为了实现随机混成系统的分析，可以通过添加概率或随机性对混成自动机进行扩展。然后对随机混成系统的验证转化成通过概率模型检验或统计模型检验进行可达性分析。但是，现有的基于随机混成系统的可达性分析\index{可达性分析}方法仍存在很多不足。
|
||
|
||
|
||
第三，如何保证具有复杂数据结构、算法或协议的系统的可靠性。现有软件系统中含有非常复杂的数据结构、算法和协议等，现有的验证理论难以完全支持。例如，操作系统内核中，为了提高系统效率，往往会使用非常复杂的指针数据结构，其复杂度远远超出双向链表、红黑树等教科书上的经典数据结构。操作系统内核和文件系统中，还会使用很多巧妙的无锁并发算法，其验证一直是形式化验证中的难点。加密算法和协议的验证则需要概率相关的特定验证理论。云计算平台中普遍使用地理上分布的多拷贝数据，其数据一致性算法的验证目前也缺少成熟理论的支持。
|
||
|
||
|
||
第四，如何保证具有复杂体系结构的系统的可靠性。复杂系统往往由大量模块构成，模块之间的组合方式复杂，总体体现为两点：（a）从纵向看，模块之间相互调用，抽象层次不同。一方面，不同抽象层次的代码特性不同，所需要的验证理论和技术也会不尽相同；另一方面，为了实现完整系统的验证，需要将这些不同抽象层次的模块验证后，得出完整系统的可靠性结论。这需要验证技术能够有效集成不同的验证方法、理论和工具，并具有很好的纵向可组合性。（b）从横向看，模块之间有多重组合方式，例如多线程并发、事件驱动等。不同的组合方式导致模块执行的控制流的多样性，这也对系统的模块化验证以及水平方向的可组合性带来挑战。
|
||
|
||
|
||
第五，如何提高软件开发的自动化程度，实现构建即正确的系统。综合(Synthesis)技术可以提高软件的自动化程度。基于演绎的方法可以从高层规范的实现中派生出低层实现；基于归纳的方法可以根据实例的行为，生成满足实例的程序。但状态空间爆炸问题制约了可综合的系统规模。符号化方法、组合式方法可以提高可综合系统的规模，却难以真正投入使用。虽然推理、求解技术的发展与硬件计算能力的提高能一定程度上推动了综合技术的应用，然而，由于可合成系统规模有限，软件的自动化仍缺乏实际应用。
|
||
|
||
|
||
最后，如何验证基于学习技术的复杂系统。机器学习的准确率难以达到百分之百。有必要对使用机器学习的系统鲁棒性进行分析。这种鲁棒性分析首先根据系统使用的神经网络结构构建相应的抽象关系，再基于抽象关系分析输入在一定的扰动下，输出是否会出现分类错误。由于复杂神经网络的神经元个数是百万级别的，而且使用了大量的非线性函数，传统的方法如基于线性规划\index{线性规划}或约束求解\index{约束求解}的方法很难实现对实际系统的分析。基于神经网络中使用的非线性函数的利普希茨(Lipschitz)连续特点对非线性函数进行抽象，或使用多面体(Zonotope)抽象表示神经网络每层的值域可以提高可分析系统的规模，但仍缺乏对实际基于学习系统的验证~\cite{Huang2018}。
|
||
|
||
\subsection{新型体系结构和计算平台下的程序语义刻画和正确性保证}\label{sec:st-architecture}
|
||
近年来，新的体系结构和计算平台大量涌现，包括多核处理器、GPU和异构芯片、分布式云计算平台\index{分布式云计算平台}等。它们对程序设计有各自特定的要求，也对相应的程序验证带来了重要的机遇和挑战。
|
||
|
||
|
||
首先，多处理器架构\index{多处理器架构}对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能~\cite{Herlihy2008}。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争\index{数据竞争}、原子性违背\index{原子性违背}、死锁\index{死锁}、活锁\index{活锁}等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言需要都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
|
||
|
||
|
||
其次，多处理架构引发了并发程序数据一致性分析的挑战。多核平台中存在多线程并发程序对共享资源的访问冲突。多线程并发程序已经成为现代程序设计的趋势。并发软件应用中的并发数据结构提供支持多线程并发访问。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。多核平台下的弱内存模型则使得多线程间数据访问的一致性难以保证。并发数据结构实现的可线性化（或其量化松弛）验证问题已经取得了一定进展，可线性化条件对有界多并发线程是可判定的，但对无界多并发线程是不可判定的。
|
||
|
||
|
||
最后，新型计算平台引发了分布式系统数据一致性分析的挑战。云计算平台中，为了提高系统的可用性，往往采用地理上分布的多拷贝数据，这也使得系统开发需要面对数据一致性、可用性和对网络分割的容忍性这三者不可兼得的经典问题（即所谓的CAP定理），需要在三者中做出取舍，取得合理折中。考虑到强数据一致性（串行一致性）的实现对效率影响较大，实际系统中往往根据业务特点来适当放松对一致性的保证，这样带来的结果是：一方面系统中可能多种一致性并存，另一方面应用级程序员在使用弱一致性数据的时候，难以保证程序业务的正确性。如何在编程语言和模型中既支持多种一致性，又能简化编程负担，并且对程序的可靠性和正确性给出指导原则和分析验证技术，是当前研究的热点。
|
||
|
||
|
||
\section{主要研究内容}
|
||
软件理论的研究与软件应用的需求、承载软件的架构、平台息息相关。如图\ref{fig:2-2-1}所示，软件理论支撑了软件应用构建的整个过程；同时，软件应用构建过程中的问题推动了软件理论的深入研究。为了应对人机物融合环境下对软件理论的诸多挑战，需要开展多方面的研究工作。首先，为了支持有效的大数据处理，需要研究针对性的算法(§\ref{sec:stc-complexity})；其次，为了保证复杂系统的可靠性，需要围绕着规约、建模、分析与验证等环节，从系统特征、行为的描述与可靠性保证方法进行研究(§\ref{sec:stc-reliability})；其次，为了支持新的处理器结构与计算平台上的程序设计，需要构建相应的理论(§\ref{sec:stc-architecture})；最后，为了提高新型软件的可靠性，需要研究新型软件的特点，从而给出相应的分析方法(§\ref{sec:stc-newsoftware})。
|
||
\begin{figure}[htbp]
|
||
\centering
|
||
\includegraphics[width=0.80\textwidth]{fig2-2/2-1.png}
|
||
\caption{软件理论的研究内容}
|
||
\label{fig:2-2-1}
|
||
\end{figure}
|
||
|
||
\subsection{面向数据科学的算法与计算复杂性理论}\label{sec:stc-complexity}
|
||
在大数据应用越来越普遍的背景下，研究面向数据科学的算法与计算复杂性理论是有效解决大数据应用问题的基础与核心。
|
||
|
||
主要研究内容包括：并行、分布式、低通信、在线、动态输入、局部计算等约束下的算法设计与分析范式；反映出这些约束的大数据计算模型中的计算复杂性下界与分类；推断、学习、统计、采样、度量等数据科学的计算原语，在大数据环境下有理论保证的高效算法与计算复杂性分析；数据依赖的算法设计和参数复杂性等非最坏情况复杂度分析理论；随机化、近似、亚线性计算及其复杂性下界；满足隐私性、公平性、容错性等理论保障的高效算法设计与分析。
|
||
|
||
\subsection{形式化方法的理论研究}\label{sec:stc-reliability}
|
||
一般来说，形式化方法的理论研究内容主要涉及规约、建模、分析与验证方法。其中，规约与建模是系统正确性、可靠性分析的基础，而分析与验证方法是保证系统正确性、可靠性的手段。
|
||
|
||
\begin{itemize}
|
||
\item 形式规约
|
||
\end{itemize}
|
||
|
||
%形式规约可以分为基于模型的方法与基于代数的方法。基于模型的方法有VDM、Z、B、CSP等。基于代数的方法有Lotos、Larch、LTL等。
|
||
为了验证不同的系统，研究人员对经典时序逻辑如LTL、CTL和CTL*等做了各种扩展上，包括博弈扩展、概率扩展、实时扩展、量子扩展等。
|
||
这些扩展在模型检验的问题复杂度高，而且有的判定问题仍未解决。
|
||
%时序逻辑的概率扩展主要包括PCTL、PCTL*等。对于离散马尔可夫链模型，PCTL的模型检验问题可在多项式时间内完成，而LTL和PCTL*的模型检验问题仍是PSPACE-完全的。时序逻辑的实时扩展，包括MTL和TCTL。MTL的可满足性问题和针对时间自动机的模型检验问题在连续时间上是不可判定的，在离散时间上是EXPSPACE-完全的。时序逻辑的量子扩展主要包括QCTL、QCTL*等。QCTL在量子马尔可夫链上的验证可在多项式时间内完成；同样，该逻辑的可满足性的判定问题目前仍然没有解决。
|
||
另外，时序逻辑的“超性质”是基于计算机安全背景的扩展，主要包括HyperLTL、HyperCTL*等。
|
||
%HyperLTL的模型检验算法在最坏情况下是非初等可判定的，同时
|
||
这两种逻辑的可满足性问题也是非初等可判定的，但对于其某些特定片段却存在较为高效的算法。%除了基于时序逻辑形式规约的研究进展，还出现了%同步语言Quartz、描述动态自适应系统的RLEAX等系统规约。此外，
|
||
%基于本体论的网络本体语言(web ontology language)用于机器人、航天领域的形式规约描述系统需求。
|
||
%近些年来，针对串行程序的形式规约语言的进展集中在分离逻辑方面。除了针对分离逻辑的研究工作，
|
||
|
||
总体来说，新出现的、更为复杂的系统特征推动了各种形式规约的提出，及对已有规约的扩展研究。但是，形式规约的表达能力越强，模型检验问题的复杂度就越高，甚至变得不可判定。如何寻找可判定的子集，在可判定的情况下，增加形式规约的表达能力，提高判定算法的效率，是该项研究的核心问题。
|
||
|
||
\begin{itemize}
|
||
\item 形式建模方法
|
||
\end{itemize}
|
||
|
||
形式建模方法用于精确地刻画计算机软硬件系统的行为。如何以数学的形式描述日益复杂的系统结构与行为，用于系统正确性分析，是形式建模研究的核心问题之一。在一些安全关键领域，为了描述和验证系统的安全性，既需要描述离散的机器指令，又需要描述系统所处环境的连续特性。通常，使用混成自动机刻画这类系统。然而，与状态机类似，混成自动机缺乏对结构的描述。因此，出现了很多辅助复杂系统模块化表示的方法。例如，支持混成行为的层次化规范的环境SHIFT、PTOLEMY，描述并发混成行为的I/O自动机、CHARON，描述混成行为的规范HCSP(Hybrid CSP)、描述基于逻辑与组合分析的混成Hoare逻辑HHL(Hybrid Hoare logic)等。工业界常使用Simulink/Stateflow环境实现复杂系统的建模，但它缺乏统一的形式语义。为了对复杂系统的建模，人们还提出了组合建模方法，如HMODEST，随机混成程序。
|
||
|
||
|
||
刻画无穷状态系统有随机、参数化等模型，除了使用相应的分析工具如INFANY、JKind等，还可以统一在进程重写系统(Process Rewrite System, PRS)中进行分析。
|
||
|
||
最近，深度神经网络的健壮性分析是研究热点之一。神经网络的结构常被表示为一组在整数域或实数域上的线性算术方程组与激活函数对应的非线性方程组的集合。然而已有的线性优化算法或者SMT求解器不擅于直接求解非线性方程。比较普遍的方法是根据具体的非线性方程，对线性优化算法或SMT求解器进行扩展，以便验证神经网络的安全性，或找到对抗干扰实例。
|
||
|
||
\begin{itemize}
|
||
\item 形式分析与验证方法
|
||
\end{itemize}
|
||
|
||
|
||
软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
|
||
|
||
1)基于符号执行的程序分析方法
|
||
|
||
符号执行提供了一种系统性遍历程序路径空间的手段。目前的研究集中在增加可分析问题类型、提高可分析程序规模与算法效率这些方面。提高可伸缩性方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码提高可伸缩性。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释\index{抽象解释}、模糊测试\index{模糊测试}、随机测试\index{随机测试}等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
|
||
|
||
2)基于抽象解释的形式验证方法
|
||
|
||
抽象解释理论为程序分析的设计和构建提供了一个通用的框架，并从理论上保证了所构建的程序分析的终止性和可靠性。抽象解释的核心问题是提高抽象的精度。为提高抽象解释分析精度，可以结合符号化方法来提高分析精度，利用SMT求解器、插值等技术来计算程序语句迁移函数的最佳抽象；也可以提高抽象域的非线性表达能力。如何有效降低存储开销和提高计算效率，是提高抽象解释可扩展性需要考虑的主要问题。在提高抽象解释的可行性方面，研究工作包括复杂数据结构如数组内容、数值与形态混合程序自动分析的支持；不同谱系目标程序如多线程程序、中断驱动型程序、概率程序的支持；活性性质如时序性质、终止性分析的支持。
|
||
|
||
3)基于演绎推理的定理证明方法
|
||
|
||
定理证明的基本思想是将程序满足其形式规约的证明问题转化为一组数学命题的证明。为了提高证明的效率、增加自动化证明程度、推广定理证明的应用，定理证明方面的研究可以分成两部分：交互式定理证明（Interactive Theorem proving）和自动推理（Automated Theorem proving）。%交互式定理证明最常用的两个证明辅助工具是Coq和Isabelle。Lean是一个最新的证明辅助工具，其中的一个设计重点是允许更有效的证明策略的实现，从而提高证明的自动化程度。
|
||
自动定理证明的基础包括SMT（Satisfiability Modulo Theories）和归结(Resolution)。SMT的研究对象是各种领域知识的逻辑组合，经常表达为带等词的一阶逻辑公式。惰性算法是目前主流的SMT求解方法，采用了被称为DPLL（T）的算法框架。为了DPLL求解与理论求解更为有效地结合，理论判定过程一般要设计为增量式的（Incremental）和可回溯的（Backtrackable）。主流SMT求解器还采用多种策略加速求解过程，如理论预处理，选择分支，理论推导，理论冲突分析和引理学习等。此外，基于定理证明的方法也可以支撑构造即正确的系统软件开发，如具有分层规范与公式推导特征的DeepSEA程序能够生成由CompCert编译的C程序、低层的Coq规范，以及表明该程序满足规范的证明。
|
||
|
||
4)基于模型检验的形式验证方法
|
||
|
||
模型检验方法的基础是状态空间的遍历。一方面，状态空间爆炸问题是大规模复杂系统模型检验方法的主要瓶颈。这方面的研究集中在怎样使用抽象或符号化等方法，减少验证过程中遍历的状态空间规模。另一方面，复杂系统中连续状态变化导致的系统可达集计算方法也相当复杂。该方面的研究主要集中在如何计算混成系统的可达集。
|
||
|
||
在缓解状态空间爆炸的方法方面，反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）是当前复杂系统模型检验的主要手段之一。同时，基于插值（Interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）也是主流的研究方向。目前相关方向的工作主要集中于如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率等。此外，通过多技术深度融合来进行代码验证是近年来的重要趋势之一。如将抽象解释（Abstract Interpretation）与模型检验相结合，将插值技术与SMT结合等等。其中最具有代表性的工作为CPAChecker工具。它基于若干技术的结合，通过统一接口集成多种求解器和技术来对软件系统进行验证，从而得到更好的性能和可伸缩性。
|
||
|
||
混成系统的可达集计算是制约混成系统验证的主要问题。
|
||
简单混成系统的验证可以通过时间自动机、多速率自动机等实现。基于决策过程的Tarski代数的方法可以计算特定线性混成系统的可达集计算。HYTECH模型检验工具是第一个实现线性混成系统的精确符号化可达性分析工具，用的是基于多面体（Polyhedral）计算的方法。而CHECKMATE、d/dt工具使用多面体方法计算线性混成系统可达集的上近似。除此以外，还可以通过惰性定理证明方法分析线性或非线性混成系统的限界可达性问题，混成系统的分析还可以采用基于网格或谓词抽象的连续动力学特性的离散化等技术。
|
||
能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，微分动态逻辑（Differential Dynamic Logic，DDL）可用于大部分混成系统的建模与自动化推理。
|
||
|
||
5)面向复杂系统的统计模型检验方法
|
||
|
||
为了避免穷举复杂系统状态而产生的空间爆炸问题，
|
||
统计模型检验方法通过有限多次的执行对系统进行模拟，并使用假设检验来推断这些样本是否提供满足或违反规范的统计证据。虽然基于仿真的解决方案并不能保证正确的结果，但可以限制发生错误的概率。而且，基于模拟的方法比基于搜索的精确方法使用的计算资源要小得多。
|
||
|
||
6)面向复杂系统的运行时验证方法
|
||
|
||
与基于模型的系统静态验证方法不同，运行时验证方法在系统运行过程中监测系统的异常，避免系统出现难以恢复的故障。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
|
||
|
||
|
||
\subsection{新型体系结构和计算平台下的程序理论}\label{sec:stc-architecture}
|
||
为了应对新涌现的体系结构与计算平台，软件与程序理论主要研究运行于新体系架构程序的语义、可靠性保证等问题。
|
||
|
||
|
||
新型体系结构下内存模型的形式化定义是软件理论研究的领域之一。片上多核／众核处理器已成为计算机体系结构发展的主流。传统的顺序一致性（Sequential Consistency）模型虽然符合程序设计的直觉，但已不能满足编译优化、处理器性能提升等多方面的需要。目前主流的多核处理器如x86、ARM和Power等所实现的内存模型都放松了对一致性的要求，允许同一线程对不同地址的读写访问可以乱序执行。在程序设计语言层面，如C11/C++11、Java等，也直接定义了内存模型，支持基于共享内存的多线程程序设计，为编译优化、虚拟机性能提升等提供必要基础。但目前，处理器及程序设计语言层面的内存模型仍缺乏严格的形式化定义，使并发程序设计及验证变得更加困难。已有的语义有x86-TSO内存模型的操作语义、Power内存模型的公理语义。但如何严格刻画不同处理器、程序设计语言的内存模型，仍有待进一步研究。
|
||
|
||
|
||
多处理器架构的并发程序可线性化问题是新型体系架构下的另一个研究内容。可线性化是多处理器并发程序设计的一种正确性条件，沿袭了顺序式程序设计的惯性，但可能会由于顺序瓶颈（Sequential Bottleneck）制约并发软件的性能和可扩展性。近年来提出的准可线性化（Quasi-linearizability）及更一般的量化松弛框架允许放松可线性化标准所要求的严格顺序规约（如放松并发队列的FIFO顺序），以适应多核平台性能优化的灵活性。可线性化问题对有界多并发线程而言是可判定的，但对无界多并发线程而言已经是不可判定的。在理论方面，已证明准可线性化问题对有界多并发线程而言是不可判定的；一般而言，弱内存模型可线性化在无界多调用/返回操作的情况下是不可判定的，但在有界多调用/返回操作的情况下是可判定的，因此可以采用静态方法来验证限界条件下并发数据结构实现的弱内存模型可线性化问题。
|
||
|
||
|
||
近年来，高性能计算机的峰值计算能力不断提高。但相关软件的发展还难以跟上。如何保证这类软件的可靠性，更是一个尚未解决的难题。目前，虽然有少量研究，但不能用于大规模并行程序的验证。
|
||
|
||
|
||
\subsection{新型软件及应用的处理与分析方法}\label{sec:stc-newsoftware}
|
||
对于近年来新出现的各种软件及应用，核心问题是在提高系统效率的同时，如何保证系统的可靠性。基于学习的系统是近期出现的主流新型软件之一。根据不同的系统需求，有不同的研究方法。
|
||
|
||
|
||
一类研究围绕着如何攻击与防御人工智能系统。基于学习的模型极易受到噪音的影响，输入中的一点噪音就会改变输出结果。因此对抗样本是不可避免的。在实际系统中，对抗样本攻击的成功率非常高。如何快速地寻找对抗样本，进行攻击，是个重要的研究问题。它本质是一个优化问题，通常可以利用梯度下降优化的方法得到较好的解。目前较新的方法将模型与噪声都转变成优化目标项，而输出限制条件转换成损失函数，值域限制被转换成了平滑截断函数的变量，这样优化器可以通过直接优化目标函数，得到对抗样本。除了对抗样本的寻找，另一个方向是如何进行防御，如对抗训练、防御蒸馏等。有研究表明，即使在有防御蒸馏保护的前提下，仍可以通过转移学习生成有效的对抗样本。
|
||
|
||
|
||
另一类研究以形式化分析为基础，提供该类系统的可靠性、鲁棒性等保证。基于神经网络的智能系统结构\index{智能系统结构}复杂，神经元结点数众多。如何验证这类系统的正确性、分析其可靠性，是一个挑战性的问题。基于抽象的方法大大提高了可处理的神经元个数。由于实际系统的输入具有不确定性，针对确定的神经网络结构判断系统对每个输入的鲁棒性难以推广，目前缺乏对实际系统可用的验证方法。一种可行的方法是对接近输出的中间层进行验证。或者，针对神经网络的可解释性问题，把语义作为训练内容，与现有的系统结合，增加网络的可解释性。另一种可行的方法是根据系统训练过程中网络结构特点，构建输出的监测器。在使用中若某个输入导致了异常的网络内部结构，则该输入可能未在训练集范围内，输出结果不一定可靠。
|
||
|
||
\section{本章小结}
|
||
计算机软硬件的飞速发展以及不同领域需求的日益复杂，催生出各种实际问题，为软件的设计与开发带来巨大的机遇与挑战。作为软件学科基础的理论与方法也需要与时俱进；我们需要不断探索解决这些挑战性问题的新途径。软件理论依赖于各种数学手段；反过来，软件及理论的发展也可能给数学研究带来新的问题。
|
||
|
||
%\section{参考文献}
|
||
%[1]. L. Peter Deutsch, Ronald B. Finkbine. ACM Fellow profile. ACM SIGSOFT Software Engineering Notes 24(1): 21 (1999).
|
||
%
|
||
%[2]. Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, Xinping Yi. A Survey of Safety and Trustworthiness of Deep Neural Networks. arXiv:1812.08342.
|
||
%
|
||
%[3]. Herlihy, Maurice, and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2011.
|