uppaal 和 spin/promela 对嵌入式系统建模的优缺点是什么？
我有点困惑-谢谢
问问题
776 次
1 回答
1
一篇过时的论文，但在比较方面有一些有用且相关的观点
http://www.brics.dk/RS/96/24/BRICS-RS-96-24.pdf
设计
考虑到设计语言，明显的区别是在 UPPAAL 中对实时系统进行建模的可能性。案例研究表明，有趣的有界活性属性可以在 UPPAAL 中表达和验证。UPPAAL 的另一个有益特性是承诺位置的可能性，这使得对案例研究中所需的广播行为进行非常自然的建模成为可能。相反，PROMELA 不能在发送和接收语句序列上应用原子性构造，因为这些语句可能会阻塞
确认
考虑到验证阶段，UPPAAL 属性语言中可表达的属性类型仅限于不变性和可能性属性。其他属性，例如我们案例研究的有界活性属性，需要表示为单独的测试自动机来探测设计。在 3.4 节中，我们介绍了如何扩展属性语言并自动生成测试自动机的想法。这在 SPIN 中已经可以用于将 LTL 属性转换为永不自动机
于 2015-12-07T18:54:02.543 回答