厉害了！扒一扒“天问一号”中的形式化验证技术
7月23日12点41分，中国首次火星探测任务“天问一号”探测器在海南文昌卫星发射中心发射升空。目前，“天问一号”已经在距离地球数百万公里之遥的奔火轨道上，极速前进，探测器各项功能及运行情况良好。
本次“天问一号”火星探测任务将一次性完成“绕、落、巡”三大任务，标志着我国行星探测的大幕正式拉开。这在世界航天史上前所未有，难度和挑战也非比寻常。
就在当天，“天问一号”瞬间刷屏。也就在那一刻，我们的团队更是激动和兴奋。因为她又一次见证了形式化验证技术的可靠性和保障性，实现了望安科技团队新的担当。在激动之余，让我们一起来扒一扒“天问一号”中的形式化验证技术。
早在2018年，望安科技创始人赵永望教授就带领团队，应邀开始启动“天问一号”关键软件内存管理子系统的形式化验证。赵教授团队将形式化验证核心技术引入到“天问一号”的操作系统领域，从数学证明的角度来验证设计领域软硬件的正确性。
通过望安科技拥有的“形式化验证”核心技术，在应用领域内，用形式化验证设计正确性的方法，改变并替代了复杂并繁琐的安全测试，从根本上来保障设计的完备性及其安全性。这也是我们的团队继载人航天工程安全关键软件验证成功后的又一次见证。
近几年来，形式化验证和方法在越来越多的领域中得以应用，尤其是保障生命、财产的重大安全领域，包括：航空航天、轨道交通、无人机/车、金融，尤其是最近区块链技术崛起，也是直接的触发因素之一。
形式化方法（Formal Methods）及基于数理逻辑进行系统规约、开发和验证的一种方法。使用形式化方法来验证设计的安全性有很大的优势，包括：可以无歧义的描述软件需求，可提供形式规约软件的一致性和准确性验证，可提供软件实现与规约之间的符合性验证，通过形式化建模和分析发现软硬件需求中存在的缺陷和错误等。
形式化验证通过清晰无歧义的形式化语言，基于形式验证方法，可以进行全自动的穷举形式验证，去保证系统无 Bug。形式化验证是安全关键系统的最佳伙伴，也是安全关键系统的最佳解决方案。目前，在操作系统和软件开发上被应用的越来越广泛。
望安科技拥有形式化验证核心技术，在领域内已达到国内、国际先进水平。可提供安全关键系统、网络、软件形式化验证技术，覆盖需求、设计、源代码的系统级形式化验证技术。公司目前基于形式化验证核心方法所研发的成果，已在航空航天、金融、芯片、物联网、无人系统、安全认证、操作系统等领域应用。
在航空航天领域已多次得以应用，包括载人航天工程安全关键软件形式化分析与验证、C919国产大飞机、航空航天的国产发动机等。并已与国内外上述领域内的企业展开了培训、研究和合作，也包括华为、蚂蚁金服、航天方舟等头部企业。公司自主研制的自动化验证工具也不断得到专业领域和使用者的关注和认可。
