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
相关论文
empty
未找到相关数据