【Java】形式化方法

形式化方法简单说就是用严格的数学与逻辑来精确描述、建模、分析并证明一个系统软件/硬件是正确的而不是只靠测试猜它“好像没问题”。目录一、一句话定义二、核心三件事1.形式规约Specification2.形式建模Modeling3.形式验证Verification三、相比于传统测试它的优势在哪1.自然语言需求2.测试3.bug发现时机四、典型应用场景高可靠/高安全五、常用技术与工具1.模型检测Model Checking2.定理证明Theorem Proving3.形式语言六、优缺点七、一句话总结一、一句话定义以形式逻辑、符号系统、集合论、自动机等为基础用无歧义的数学语言对系统进行规约、建模、验证与开发的工程方法。二、核心三件事1.形式规约Specification用形式语言如Z、VDM、时序逻辑写清楚系统要做什么、不能做什么无歧义、可机器处理。2.形式建模Modeling把系统抽象成数学模型状态机、迁移系统、Petri网、进程代数等。3.形式验证Verification用数学证明或自动工具模型检测、定理证明器证明模型满足规约不存在死锁、越界、数据竞争、安全漏洞等。三、相比于传统测试它的优势在哪1.自然语言需求有歧义、不完备→ 形式规约精确、无二义。2.测试只能测“已想到的用例”测不完所有情况→ 形式验证数学上证明所有情况都正确。3.bug发现时机测试阶段甚至上线后→ 建模/设计阶段就发现成本低。四、典型应用场景高可靠/高安全1.航空飞控软件、机载系统2.高铁信号连锁、自动驾驶3.芯片CPU/总线设计如Intel用它避免浮点错误4.医疗心脏起搏器、放疗设备软件5.区块链智能合约安全审计防重入、溢出6.操作系统微内核、驱动模块验证五、常用技术与工具1.模型检测Model Checking遍历有限状态空间自动找反例工具SPIN、NuSMV。2.定理证明Theorem Proving用逻辑推导证明无限状态系统工具Coq、Isabelle。3.形式语言Z、B、VDM、CSP、TLA。六、优缺点优点精确、可证、早发现错误、高可信。缺点学习曲线陡、建模成本高、大规模系统建模难一般只在关键模块用。七、一句话总结形式化方法 把系统变成数学对象用数学证明它“一定正确”而不是“测出来没出错”。