A Case Study in Refinement-Based Modelling of a Resilient Control System

详细信息    查看全文

• 作者：Yuliya Prokhorova (18) (19)
  Elena Troubitsyna (19)
  Linas Laibinis (19)
  
• 关键词：Event ; B ; formal modelling ; refinement ; resilient control systems ; steam boiler
• 刊名：Lecture Notes in Computer Science
• 出版年：2013
• 出版时间：2013
• 年：2013
• 卷：8166
• 期：1
• 页码：94-108
• 全文大小：254KB
• 参考文献：1. Laprie, J.: From Dependability to Resilience. In: Proceedings of the 38th IEEE/IFIP International Conference on Dependable Systems and Networks, pp. G8鈥揋9 (2008)
  2. Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010) CrossRef
  3. Abrial, J.R.: Steam-Boiler Control Specification Problem. In: Abrial, J.-R., B枚rger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol.聽1165, pp. 500鈥?09. Springer, Heidelberg (1996) CrossRef
  4. Event-B and the Rodin Platform (2013), http://www.event-b.org/
  5. Storey, N.: Safety-Critical Computer Systems. Addison-Wesley, Harlow (1996)
  6. Prokhorova, Y., Troubitsyna, E., Laibinis, L.: A Case Study in Refinement-Based Modelling of a Resilient Control System. Technical Report TUCS 1086 (2013)
  7. Lopatkin, I., Prokhorova, Y., Troubitsyna, E., Iliasov, A., Romanovsky, A.: Patterns for Representing FMEA in Formal Specification of Control Systems. Technical Report TUCS 1003 (2011)
  8. Ji, K., Lu, Y., Liao, L., Song, Z., Wei, D.: Prognostics Enabled Resilient Control for Model-Based Building Automation Systems. In: Proceedings of Building Simulation 2011: 12th Conference of International Building Performance Simulation Association, pp. 286鈥?93 (2011)
  9. Cordy, M., Classen, A., Heymans, P., Legay, A., Schobbens, P.-Y.: Model Checking Adaptive Software with Featured Transition Systems. In: C谩mara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems. LNCS, vol.聽7740, pp. 1鈥?9. Springer, Heidelberg (2013) CrossRef
  10. Abrial, J.-R., B枚rger, E., Langmaack, H. (eds.): Dagstuhl Seminar 1995. LNCS, vol.聽1165. Springer, Heidelberg (1996)
  
• 作者单位：Yuliya Prokhorova (18) (19)
  Elena Troubitsyna (19)
  Linas Laibinis (19)
  
  18. Turku Centre for Computer Science, TUCS, Finland
  19. Department of Information Technologies, 脜bo Akademi University, Joukahaisenkatu 3-5 A, 20520, Turku, Finland
  
• ISSN：1611-3349

文摘

In this paper, we present a case study in modelling a resilient control system in Event-B. We demonstrate how to formally define the basic safety properties and fault tolerance mechanisms, as well as the system modes describing the system behaviour under different execution and fault conditions. Our formal development helps us to identify the diagnosability conditions for resilience, i.e., identify the limitations to be imposed on possible component changes to guarantee its controllability and hence dependability.