NIST Special Publication 800-53 Revision 5.2.0 Rev 5.2.0

形式化模型使用形式化语言描述特定的行为或安全与隐私策略，从而使这些行为和策略的正确性能够被形式化地证明。并非系统的所有组件都可以被建模。通常，形式化规范的范围限于所关注的行为或策略，例如非自主访问控制策略。组织根据要描述的行为和政策的性质以及可用的工具来选择正式建模语言和方法。