NIST的Raphael Barbau和Conrad Bock受邀在马里兰大学设计表现前沿暑期学校展示NIST开发的软件,该软件有助于发现系统行为设计中的不一致性。这个为期一周的活动聚焦于帮助工程设计的新兴数学、统计和计算基础。
从OBM到SMT的NIST软件自动转换器旨在与系统建模语言(SysML)一起使用,SysML是一种广泛使用的标准,用于指定需求,设计和测试复杂系统。该软件利用了Bock在SysML之前的工作中开发的技术,本体行为建模(OBM),它为表达系统行为提供了数学基础。Barbau的软件在此基础上将系统行为转换为广泛使用的文件格式,用于陈述可满足模数理论(SMT)中的逻辑问题,SMT是布尔可满足性(SAT)的更一般形式。
一旦工程师们应用了NIST的基于sysml的方法来设计一个复杂的系统,他们就可以使用NIST的软件来自动检测系统行为指定方式中的不一致性。该软件将SysML模型转换为逻辑问题,然后使用开源逻辑求解器通过自动推理找到不一致之处,以便工程师纠正系统的设计。