资料下载
基于SPARDL的Event-B解释
分享资料个
在软件的生命周期内，从需求分析到软件维护的任何阶段，都可能存在漏洞。因此工程师们期望在软件运行中尽可能早地（最好是在需求分析阶段）检测到错误。面对这样的挑战，本文提出一种用需求建模语言SPARDL用于为周期性控制系统建模。
SPARDL是一种用于控制系统的需求建模语言，尤其适用于基于模式的、有着混合的（连须的／离散的）状态、有限的周期行为和通信特征的控制系统。在每个周期中，系统都会并且只会精确地处在一个模式下，它可以停留在这个模式或者根据它现在的状态转换到另一个模式。作为一个轻量级的形式化语言，SPARDL可以在需求阶段消除不确定性，而这通常对于系统的正确性来说是一个挑战。
Event-B是一个重量级的形式化语言，它基于传统的谓词演算和定理证明。在Event-B中，事件（event）足一个主要的特征，因此它非常适合用来为周期行为建模。另外，Event-B还支持逐步精化地建立系统模型。用户可以在建模之初构建一个粗略的原型，然后不断地使用精化策略，使之成为一个更为复杂但实用的系统。在软件开发模型中，增量开发是运用于复杂系统开发的常见方式，能够极大地减少漏洞的出现。
Event-B中的精化机制使得在形式化的建模和分析中进行增量开发变得方便。本文首先根据基本需求建立一个粗略的SPARDL的Event-B模型，然后再根据更多的需求精化这个模型。用Event-B为SPARDL系统建模，可以在一定程度上用它对应的Rodin平台验证控制系统的需求。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
- 相关下载
- 相关文章
