Correct Pattern-Based Development Through Refinements and Weakest Preconditions Calculus

被引:0
|
作者
Fares, Elie [1 ,2 ]
Bodeveix, Jean-Paul [2 ,3 ]
Filali, Mamoun [3 ]
机构
[1] Higher Coll Technol, Ras Al Khaymah, U Arab Emirates
[2] IRIT UPS Univ Toulouse, Toulouse, France
[3] Univ Toulouse, IRIT CNRS, Toulouse, France
来源
FORMAL ASPECTS OF COMPONENT SOFTWARE, FACS 2024 | 2024年 / 15189卷
关键词
Formal requirements; Event-B; Patterns; Weakest preconditions calculus; EVENT-B; AUTOMATIC REFINEMENT;
D O I
10.1007/978-3-031-71261-6_4
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper focuses on the preliminary steps of developing safety-critical systems. We investigate how patterns could be used to generate Event-B refinements automatically. The patterns proposed in this paper either impose constraints on the model through weakest precondition calculus, superpose counters, or introduce de-synchronization mechanisms using observers. We show how the weakest precondition calculus integrated into the patterns can be simplified and become usable. Moreover, for our patterns to be fully usable in subsequent refinement steps, we produce as much as possible readable Event-B models. Finally, we revisit a classic case study using our proposed patterns.
引用
收藏
页码:59 / 78
页数:20
相关论文
共 50 条
  • [31] Pattern-based collaboratffon in ad-hoc teams through message annotation
    Schall, Daniel
    Gornbotz, Robert
    Dustdar, Schahrain
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: SOFTWARE AGENTS AND INTERNET COMPUTING, 2007, : 84 - 91
  • [32] Exploring the Applicability of Pattern-Based Business Model Development in the Smart Home Domain
    Chasin, Friedrich
    Paukstadt, Ute
    Knauth, Paul
    Becker, Jorg
    2020 IEEE 22ND CONFERENCE ON BUSINESS INFORMATICS (CBI 2020), VOL I - RESEARCH PAPERS, 2020, : 124 - 133
  • [33] Dealing with Abstract Interaction Modeling in an MDE Development Process: A Pattern-Based Approach
    Valverde, Francisco
    Panach, Ignacio
    Aquino, Nathalie
    Pastor, Oscar
    NEW TRENDS ON HUMAN-COMPUTER INTERACTION: RESEARCH, DEVELOPMENT, NEW TOOLS AND METHODS, 2009, : 119 - 128
  • [34] PATTERN-BASED DEVELOPMENT OF ENTERPRISE SYSTEMS From Conceptual Framework to Series of Implementations
    Zykov, Sergey V.
    ICEIS 2011: PROCEEDINGS OF THE 13TH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS, VOL 4, 2011, : 475 - 478
  • [35] From model to requirements: Pattern-based analysis in distributed development of embedded systems
    Thomsen, C
    Kruse, J
    Ernst, R
    From Specification to Embedded Systems Application, 2005, 184 : 35 - 44
  • [36] A Model- and Pattern-based Approach for Development of User Interfaces of Interactive Systems
    Engel, Juergen
    EICS 2010: PROCEEDINGS OF THE 2010 ACM SIGCHI SYMPOSIUM ON ENGINEERING INTERACTIVE COMPUTING SYSTEMS, 2010, : 337 - 340
  • [37] Development of a behaviour pattern-based testing approach for coupled socioeconomic and environmental models
    Alizadeh, Mohammad Reza
    Peng, Xingyu
    Adamowski, Jan
    Albano, Raffaele
    Ozga-Zielinski, Bogdan
    Inam, Azhar
    JOURNAL OF ENVIRONMENTAL MANAGEMENT, 2023, 347
  • [38] Security patterns modeling and formalization for pattern-based development of secure software systems
    Hamid, B.
    Guergens, S.
    Fuchs, A.
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2016, 12 (02) : 109 - 140
  • [39] Pattern-based Business Model Development for Cyber-Physical Production Systems
    Rudtsch, Vinzent
    Gausemeier, Juergen
    Gesing, Judith
    Mittag, Tobias
    Peter, Stefan
    8TH INTERNATIONAL CONFERENCE ON DIGITAL ENTERPRISE TECHNOLOGY - DET 2014 DISRUPTIVE INNOVATION IN MANUFACTURING ENGINEERING TOWARDS THE 4TH INDUSTRIAL REVOLUTION, 2014, 25 : 313 - 319
  • [40] A pattern-based object-linking mechanism for component-based software development environments
    Fruth, LS
    Purtilo, JM
    White, EL
    JOURNAL OF SYSTEMS AND SOFTWARE, 1996, 32 (03) : 227 - 235