Formal Goal-Oriented Development of Resilient MAS in Event-B

详细信息    查看全文

• 作者：Inna Pereverzeva (12) inna.pereverzeva@abo.fi
  Elena Troubitsyna (2) elena.troubitsyna@abo.fi
  Linas Laibinis (2) linas.laibinis@abo.fi
• 关键词：Event ; B – ; formal modelling – ; refinement – ; goal ; oriented development – ; multi ; agent system
• 刊名：Lecture Notes in Computer Science
• 出版年：2012
• 出版时间：2012
• 年：2012
• 卷：7308
• 期：1
• 页码：147-161
• 全文大小：253.3 KB
• 参考文献：1. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (2005)
  2. Abrial, J.R.: Modeling in Event-B. Cambridge University Press (2010)
  3. Ball, E., Butler, M.: Event-B Patterns for Specifying Fault-Tolerance in Multi-agent Interaction. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 104–129. Springer, Heidelberg (2009)
  4. EU-project DEPLOY: http://www.deploy-project.eu/
  5. van Lamsweerde, A.: Goal-oriented requirements engineering: A guided tour. In: Requirements Engineering, pp. 249–263 (2001)
  6. Landtsheer, R.D., Letier, E., van Lamsweerde, A.: Deriving tabular event-based specifications from goal-oriented requirements models. In: Requirements Engineering, p. 200 (2003)
  7. Laprie, J.: From dependability to resilience. In: 38th IEEE/IFIP Int. Conf. On Dependable Systems and Networks, pp. G8–G9 (2008)
  8. Matoussi, A., Gervais, F., Laleau, R.: A Goal-Based Approach to Guide the Design of an Abstract Event-B Specification. In: 16th International Conference on Engineering of Complex Computer Systems, pp. 139–148. IEEE (2011)
  9. OMG Mobile Agents Facility (MASIF): http://www.omg.org
  10. Ponsard, C., Dallons, G., Philippe, M.: From Rigorous Requirements Engineering to Formal System Design of Safety-Critical Systems. ERCIM News (75), 22–23 (2008)
  11. Rodin: Event-B Platform: http://www.event-b.org/
  12. Roman, G.-C., Julien, C., Payton, J.: A Formal Treatment of Context-Awareness. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 12–36. Springer, Heidelberg (2004)
  13. Roman, G.C., Julien, C., Payton, J.: Modeling Adaptive Behaviors in Context UNITY. Theoretical Computure Science 376, 185–204 (2007)
  14. Roman, G.C., McCann, P., Plun, J.: Mobile UNITY: Reasoning and Specification in Mobile Computing. ACM Transactions of Software Engineering and Methodology, 250–282 (1997)
  15. Vain, J., Tammet, T., Kuusik, A., Juurik, S.: Towards scalable proofs of robot swarm dependability. In: BEC 2008, pp. 199–202 (2008)
• 作者单位：1. Turku Centre for Computer Science, Finland2. 脜bo Akademi University, Joukahaisenkatu 3-5, 20520 Turku, Finland
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Goal-Oriented Development facilitates structuring complex requirements. To ensure resilience the designers should guarantee that the system achieves its goals despite changes, e.g., caused by failures of system components. In this paper we propose a formal goal-oriented approach to development of resilient MAS. We formalize the notion of goal and goal achievement in Event-B and propose the specification and refinement patterns that allow us to guarantee that the targeted goals are reached despite agent failures. We illustrate our approach by a case study – development of an autonomous multi-robotic system.