193 lines
39 KiB
TeX
193 lines
39 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{复杂性理论}支持海量数据的高效处理\cite{chen2014data}；云端计算的发展需要新型的分布式计算理论\index{计算理论}以及新型的编程模型；人工智能的发展使得具有不确定性的知识表示和推理成为一种常规的思维方式，从而给算法和复杂性理论、编程模型以及软件的可靠性分析\index{软件可靠性}等带来众多问题\cite{arpteg2018software}；信息物理融合系统（CPS）\index{信息物理融合系统}和物联网应用则使得既有离散事件又有连续状态变化的混成系统\index{混成系统系统}的建模、分析和验证成为难以回避的挑战\cite{lunze2009handbook}。
|
||
|
||
|
||
其次，软件运行环境和硬件平台的变革为软件理论带来挑战。一方面，处理器能力和网络带宽的大幅提升，使得以往受限于计算或通信能力的技术变得更具有实用性，包括：特定的编程模型以及程序的自动化分析和验证技术，从而为软件理论的发展带来新的驱动力。另一方面，硬件平台和运行环境的变革也带来巨大挑战，为软件的规约、建模、分析和验证带来困难，包括：多核处理器的普及促进了并发程序的使用，但对于高效并发算法的验证缺少理论和工具支持\cite{herlihy2011art}；其他还包括：搭载异构芯片的处理器、云平台上数据一致性的形式化规约和验证等。
|
||
|
||
|
||
其三，软件基础性地位的提升为软件理论带来挑战。软件作为基础设施，日益深入到我们生产生活的方方面面，相应地，对软件可靠性的要求也变得越来越强。人们开始期望那些在以往仅仅针对特定算法和协议的验证技术能够应用于代码级的完整的全栈系统验证上，特别是底层系统软件的验证，如操作系统内核、编译器\index{编译器}、密码算法和协议实现等\cite{sewell2013translation}。基于学习的人工智能技术在自动驾驶等安全攸关系统中的应用使得混成系统和概率系统的形式验证需求越发迫切\cite{koopman2017autonomous}。同时，软件复杂度的提高，对于可信软件的自动化开发和验证技术也提出了更高的要求。
|
||
|
||
|
||
本章将针对软件理论的核心内容，包括算法及复杂性理论、程序正确性理论等，逐一探讨其面临的挑战，以及将来需要开展的研究。
|
||
|
||
|
||
\section{重大挑战问题}
|
||
在新的时代背景下，特别是在人机物融合的大环境下，软件理论遇到了新的挑战。具体包括：如何应对大规模的数据与计算(§\ref{sec:st-complexity})；如何保证复杂软件系统的正确性、可靠性、安全性(§\ref{sec:st-reliability})；针对新型计算机的硬件架构与新的计算平台，如何建立其理论分析基础(§\ref{sec:st-architecture})；如何分析新型计算模型下的程序并保证它的正确性(§\ref{sec:st-quantum})。
|
||
%
|
||
|
||
\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{huang2017}。
|
||
|
||
\subsection{新型体系结构和计算平台下的程序语义刻画和正确性保证}\label{sec:st-architecture}
|
||
近年来，新的体系结构和计算平台大量涌现，包括多核处理器、GPU和异构芯片、分布式云计算平台\index{分布式云计算平台}等。它们对程序设计有各自特定的要求，也对相应的程序验证带来了重要的机遇和挑战。
|
||
|
||
|
||
首先，多处理器架构\index{多处理器架构}对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能~\cite{Herlihy2008}。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争\index{数据竞争}、原子性违背\index{原子性违背}、死锁\index{死锁}、活锁\index{活锁}等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
|
||
|
||
|
||
其次，多处理器架构引发了并发程序数据一致性分析的挑战。多核平台中存在多线程并发程序对共享资源的访问冲突。多线程并发程序已经成为现代程序设计的常态。并发软件应用中的并发数据结构提供支持多线程并发访问。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。多核平台下的弱内存模型则使得多线程间数据访问的一致性难以保证。并发数据结构实现的可线性化（或其量化松弛）验证问题已经取得了一定进展，可线性化条件对有界多并发线程是可判定的，但对无界多并发线程是不可判定的。
|
||
|
||
|
||
最后，新型计算平台引发了分布式系统数据一致性分析的挑战。云计算平台中，为了提高系统的可用性，往往采用地理上分布的多拷贝数据，这也使得系统开发需要面对数据一致性、可用性和对网络分割的容忍性这三者不可兼得的经典问题（即所谓的CAP定理），需要在三者中做出取舍，取得合理折中。考虑到强数据一致性（串行一致性）的实现对效率影响较大，实际系统中往往根据业务特点来适当放松对一致性的保证，这样带来的结果是：一方面系统中可能多种一致性并存，另一方面应用级程序员在使用弱一致性数据的时候，难以保证程序业务的正确性。如何在编程语言和模型中既支持多种一致性，又能简化编程负担，并且对程序的可靠性和正确性给出指导原则和分析验证技术，是当前研究的热点。
|
||
|
||
\subsection{新型计算模型下的计算复杂性理论与程序正确性保证}\label{sec:st-quantum}
|
||
随着量子硬件设计与制造技术的飞速发展，人们乐观地预测多于一百个量子比特的特定用途的量子计算机有望在5-10 年内实现。量子计算拟充分利用量子力学的两大特性——量子叠加与量子纠缠——来获得潜在的比传统计算性能上的大幅度提升，从而有可能使用量子计算模型来解决经典计算模型中无法高效计算的问题\cite{montanaro2016quantum}，特别是一些经典困难问题，例如Shor提出的量子整数分解算法~\cite{lomonaco2002shor}可以高效地求解大整数的质因数分解问题，Grover提出的量子搜索算法~\cite{grover1996fast}可以开平方根量级的加速无序数组的查找问题。
|
||
|
||
量子软件与算法领域最核心的挑战问题仍然是：量子软件与算法能否比经典软件算法在效率上有本质的提升？如果可以提升，那在哪些问题上可以有提升？最多可以提升多大量级？即能否从数学上完全刻画出量子计算能够有效加速的范围及其加速的极限。这对于我们更加深刻的理解计算的本质，特别是计算困难性的起源有着重要的科学意义。同时它还有助于加深我们对于量子力学本质的认识，以及在宏观尺度下量子效应的展示。
|
||
|
||
另一个重要的挑战是量子软件和程序该如何进行验证~\cite{ying2016foundations}。虽然量子程序的分析与形式验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，很多问题甚至还不清楚如何准确定义。对于整数分解问题，因其属于NP复杂性类，其结果可以有效地经典验证，但是对一个超出经典计算机能力的量子程序，如何才能验证其正确性？例如最近谷歌宣称的“量子优越性”实验。量子密码协议，特别是量子密钥分发协议从理论上具有比经典协议更好的安全性保障，但如何才能够使用经典的方式来验证所设计的量子密码协议的正确性？
|
||
|
||
%第三个重要的挑战是如何进行量子的编译和电路优化。谷歌等公司已经能制造出53-70物理比特的量子芯片，量子计算的发展目前正在进入到含噪中尺度量子系统时代 (NISQ, Noisy Intermediate-Scale Quantum Computing)。目前的量子纠错方法或者纠错成本过高（需要约100：1的纠错比特开销），或者所需要的物理比特的质量要求过高（需要门正确率阈值超过3个9以上）。如何能够通过电路的优化和软件编译的优化使得在NISQ系统上真正运行一个有意义的量子软件和算法？
|
||
\section{主要研究内容}
|
||
软件理论的研究与软件应用的需求、承载软件的架构、平台息息相关。如图\ref{fig:2-2-1}所示，软件理论支撑了软件语言、软件构建与运行原理的整个体系；同时，软件技术和系统的问题推动了软件理论的深入研究。为了应对人机物融合环境下对软件理论的诸多挑战，需要开展多方面的研究工作。首先，为了支持有效的大数据处理，需要研究针对性的算法(§\ref{sec:stc-complexity})；其次，为了保证复杂系统的可靠性，需要围绕着规约、建模、分析与验证等环节，从系统特征、行为的描述与可靠性保证方法等方面进行研究(§\ref{sec:stc-reliability})；为了支持新的处理器结构与计算平台、新型计算模型上的程序设计，需要构建相应的理论(§\ref{sec:stc-architecture}, §\ref{sec:stc-quantum})；最后，为了提高新型软件的可靠性，需要研究新型软件的特点，从而给出相应的分析方法(§\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}
|
||
%
|
||
%
|
||
%软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。
|
||
|
||
形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。基于符号执行的程序分析方法研究集中在增加可分析问题类型、提高可分析程序规模与算法效率这些方面。基于抽象解释的形式验证主要包括提高抽象精度与可行性方面的研究。基于演绎推理的定理证明研究包括如何采用多种策略加速求解过程，如何支撑构造即正确的系统软件开发。基于模型检验的形式验证研究包括使用抽象或符号化等方法减少验证过程中遍历的状态空间规模、计算混成系统的可达集等。此外，还需研究约束求解及解计数技术，特别是可满足性判定（SAT/SMT）方法。
|
||
|
||
%\begin{itemize}
|
||
%\item 基于符号执行的程序分析方法研究集中在增加可分析问题类型、提高可行性、可分析程序规模与算法效率这些方面。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。提高可分析程序规模方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码等。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释\index{抽象解释}、模糊测试\index{模糊测试}、随机测试\index{随机测试}等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
|
||
%
|
||
%\item 基于抽象解释的形式验证主要包括提高抽象精度与可行性方面的研究。提高抽象解释分析精度的方法包括结合符号化方法来提高分析精度，利用SMT求解器、插值等技术来计算程序语句迁移函数的最佳抽象；提高抽象域的非线性表达能力。提高抽象解释可行性方面的研究工作包括复杂数据结构如数组内容、数值与形态混合程序自动分析的支持；不同谱系目标程序如多线程程序、中断驱动型程序、概率程序的支持；活性性质如时序性质、终止性分析的支持。
|
||
%
|
||
%\item 基于演绎推理的定理证明研究可以分成两部分：交互式定理证明（Interactive Theorem proving）和自动推理（Automated Theorem proving）。%交互式定理证明最常用的两个证明辅助工具是Coq和Isabelle。Lean是一个最新的证明辅助工具，其中的一个设计重点是允许更有效的证明策略的实现，从而提高证明的自动化程度。
|
||
%自动定理证明的基础包括SMT（Satisfiability Modulo Theories）和归结(Resolution)。SMT的研究包括如何将已有的算法框架与理论求解有效结合，如何采用多种策略加速求解过程，如理论预处理，选择分支，理论推导，理论冲突分析和引理学习等。 基于定理证明的研究主要围绕如何支撑构造即正确的系统软件开发。
|
||
%
|
||
%\item 基于模型检验的形式验证研究包括使用抽象或符号化等方法减少验证过程中遍历的状态空间规模、计算混成系统的可达集等。在缓解状态空间爆炸的研究包括反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）、基于插值（Interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）、如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率、如何通过多技术深度融合来进行代码验证、如何将抽象解释（Abstract Interpretation）与模型检验相结合、如何将插值技术与SMT结合等等。
|
||
%混成系统的可达集计算包括使用基于决策过程的Tarski代数方法、基于多面体（Polyhedral）的计算、通过惰性定理证明方法分析线性或非线性混成系统的限界可达性问题、采用基于网格或谓词抽象的连续动力学特性的离散化等技术。
|
||
%
|
||
%\item 面向复杂系统的统计模型检验研究内容包括功能与非功能规约的形式化表示、涵盖功能与非功能规约的统一模型、统计模型检测算法的改进、确认正确(Verified)的工具实现、不同领域的应用等。
|
||
%
|
||
%\item 面向复杂系统的运行时验证研究包括如何降低监测对系统的开销、如何实现对实时系统的监测、如何对新型软件如基于学习的系统的监测等。
|
||
%\end{itemize}
|
||
|
||
|
||
\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-quantum}
|
||
针对量子计算模型下的挑战性问题，具体研究内容如下：量子程序设计与验证、量子密码协议设计与验证、量子复杂性下界问题等。量子程序设计与验证的研究包括量子程序设计模型和基本指令集；适用于量子计算的程序逻辑；量子程序不变式生成问题；量子程序的模型检验问题；并行与分布式量子程序设计技术等。量子密码协议设计与验证的研究包括抗量子攻击的经典密码协议，量子随机数生成，量子密码协议验证，量子纠错与编码等。量子复杂性下界研究包括图灵机模型下量子与经典复杂性类的（神谕）区分；量子通信协议复杂性下界；量子判定树模型复杂性下界；量子计算的交互式验证等。
|
||
|
||
\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.
|