Modal Systems: Specification, Refinement and Realisation
Modal Systems: Specification, Refinement and Realisation
复制标题
模态系统：规范、细化和实现
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Romanovsky
中科院分区：
文献类型：
--
作者：
F. Dotti;A. Iliasov;L. Ribeiro;A. Romanovsky
操作模式是有用的结构化单元，其促进了诸如航空电子、运输和空间系统等若干安全关键系统的设计。虽然在文献中可以找到一些支持模态系统的建设，建模抽象的形式规范，分析和正确的模态系统的建设仍然缺乏。
本文讨论了现有的支持模态系统的建设，并提出了一个形式化和完善的概念模态系统。一个模态系统，指定使用建议的抽象，可以实现使用不同的规范语言。补充的贡献，我们定义了一个事件-B模型实现一个模态系统规范的要求。一个案例研究说明了所提出的方法。
Operation modes are useful structuring units that facilitate design of several safety-critical systems such as such as avionic, transportation and space systems. Although some support to the construction of modal systems can be found in the literature, modelling abstractions for the formal specification, analysis and correct construction of modal systems are still lacking.
This paper discusses existing support for the construction of modal systems and proposes both a formalisation and a refinement notion for modal systems. A modal system, specified using the proposed abstractions, can be realised using different specification languages. Complementing the contribution, we define the requirements for an Event-B model to realise a modal system specification. A case study illustrates the proposed approach.