FSV1, FSUZ_Lightfoot_01
软件工程师的主要目标是开发一个可靠的系统，形式化方法用来规范和验证系统，帮助工程师建造更可靠的系统。
检查设计的整个状态空间的方法：对任何可能的输入都是正确且安全的。
形式化方法可以应用于整个开发过程的各个点。
规格说明是一种客户需求的描述，可能以某种符号（语言）编写，可能是功能需求、安全需求、效率需求或实现需求：
规格说明作为约定：
规格说明的目标：以简洁、清晰、明确的方式捕捉客户的需求，以最大限度地减少软件系统开发过程中的失败风险。
规格说明的优点：
规格说明的认可（validation）：符合客户需求。
规格说明的满足：形式化提炼（refine）、非形式化测试。