基于状态图转形式化B模型的安全苛求系统开发方法

doi:10.19678/j.issn.1000-3428.0068642

摘要/Abstract

摘要：

形式化方法精确且严格, 较多应用于安全苛求系统开发, 但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题, 提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法, 从而结合状态图的易用性降低在安全苛求软件系统开发过程中使用形式化方法的复杂度。该转译方法分为映射规则、同步语义和程序实现3个部分, 以保证自动转译后的模型自身含义与基础语义不变。在平交道口控制系统开发案例分析中, 该方法根据图元模型自动生成了对应形式化模型, 通过对形式化模型的分析改进系统在功能安全、数据安全、隐藏分支3个方面的非安全因素, 并保证从需求至模型的一致性, 证明了该方法可降低形式化方法建模难度, 提高软件系统的正确性、可靠性与安全性。

关键词: 软件功能安全, 形式化方法, 模型转化, SCXML状态图, B方法

Abstract:

The formal method is widely used to develop safety-critical systems because it is rigorous and precise. However, it has high learning costs, high complexity, and low reusability. The commonly used informal state chart model is easy to use but lacks rigorous verification. Thus, we propose an approach to automatically translate the SCXML model into the B formal model. The aim is to combine the ease of use of the state chart to reduce the complexity of formal methods when developing safety-critical software systems. The translation method is elaborated in three parts: mapping rules, synchronous semantics, and program implementation, to ensure that the meaning and basic semantics of the model do not change after automatic translation. In the case analysis of developing a level crossing control system, the method automatically generates a corresponding formal model according to the original state chart, improving functional safety, data security, and the three unsafe aspects of hidden branches through the analysis of the formal model, while ensuring consistency with model requirements. This method reduces the modeling complexity of the formal method and enhances the correctness, reliability, and safety of software systems.

Key words: software functional safety, formal method, model transformation, State Chart extensible Markup Language(SCXML) state chart, B method

赵大地, 王恪铭. 基于状态图转形式化B模型的安全苛求系统开发方法[J]. 计算机工程, 2024, 50(11): 173-186.

ZHAO Dadi, WANG Keming. Safety-Critical System Development Method Based on Translating State Chart to B Formal Model[J]. Computer Engineering, 2024, 50(11): 173-186.

https://www.ecice06.com/CN/Y2024/V50/I11/173

图/表 11

图1 计时器SCXML模型

Fig.1 Timer SCXML model

图2 B抽象机文件

Fig.2 B abstract machine file

图3 总体映射思路

Fig.3 General approach of mapping

图4 道口控制系统

Fig.4 Control system of railway level crossing

图5 监视器状态图模型

Fig.5 State chart model of monitor

图6 原始证明结果图

Fig.6 Diagram of prove results of previous version

图7 模型缺陷导致不能通过的证明义务

Fig.7 Proof obligations unpassed due to model defects

图8 缺少数据限定导致不能通过的证明义务

Fig.8 Proof obligations unpassed due to lack data limitation

图9 忽略隐藏危险分支导致不能通过的证明义务

Fig.9 Proof obligations unpassed due to hidden dangerous branch

图10 证明结果图

Fig.10 Diagram of prove results

图11 添加语义验证不变式的证明结果图

Fig.11 Diagram of prove results after adding semantic verification invariant

参考文献 34

1	王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌. 软件学报, 2019, 30 (1): 33- 61. doi: 10.13328/j.cnki.jos.005652
	WANG J, ZHAN N J, FENG X Y, et al. Overview of formal methods. Journal of Software, 2019, 30 (1): 33- 61. doi: 10.13328/j.cnki.jos.005652
2	WANG K M, WANG X, WANG Z, et al. Logical consistency verification of state sensing in safety-critical decision: a case study of train routing selection. IET Intelligent Transport Systems, 2022, 16 (8): 1042- 1057. doi: 10.1049/itr2.12194
3	WOODCOCK J, STEPNEY S, COOPER D, et al. The certification of the Mondex electronic purse to ITSEC level E6. Formal Aspects of Computing, 2008, 20 (1): 5- 19. doi: 10.1007/s00165-007-0060-5
4	BONFANTI S, GARGANTINI A, MASHKOOR A. A systematic literature review of the use of formal methods in medical software systems. Journal of Software: Evolution and Process, 2018, 30 (5): e1943. doi: 10.1002/smr.1943
5	BOLTON M L, MOLINARO K A, HOUSER A M. A formal method for assessing the impact of task-based erroneous human behavior on system safety. Reliability Engineering & System Safety, 2019, 188, 168- 180. doi: 10.1016/j.ress.2019.03.010
6	闫倩倩, 缪炜恺. 轨道交通控制软件中基于场景的需求分析方法. 计算机工程, 2021, 47 (8): 284-293, 300. doi: 10.19678/j.issn.1000-3428.0058548
	YAN Q Q, MIAO W K. Scenario-based requirement analysis method for railway control software. Computer Engineering, 2021, 47 (8): 284-293, 300. doi: 10.19678/j.issn.1000-3428.0058548
7	ESTEFAN J A. Survey of Model-Based Systems Engineering(MBSE) methodologies. INCOSE MBSE Focus Group, 2007, 25 (8): 1- 12.
8	CZARNECKI K, HELSEN S. Classification of model transformation approaches[C]//Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture. Atlanta, USA: [s. n.], 2003: 1-17.
9	TORRE D, GENERO M, LABICHE Y, et al. How consistency is handled in model-driven software engineering and UML: an expert opinion survey. Software Quality Journal, 2023, 31 (1): 1- 54. doi: 10.1007/s11219-022-09585-2
10	ELTAYEB A R, COLOMB R M. Automating the path from models to executable systems in MDA approach[C]//Proceedings of the JCCO Joint International Conference on ICT in Education and Training, International Conference on Computing in Arabic, and International Conference on Geocomputing. Washington D. C., USA: IEEE Press, 2018: 1-7.
11	SAITOV E B, SODIQOV T B. Modeling an autonomous photovoltaic system in the MATLAB Simulink software environment[C]//Proceedings of 2021 Asia-Pacific Conference on Applied Mathematics and Statistics. Chiangmai, Thailand: AIP Publishing, 2022: 249835753.
12	van DOC V, QUYET T H, TRONG B N. Development of the rules for transformation of UML sequence diagrams into queueing Petri nets[C]//Proceedings of INISCOM 2018. Berlin, Germany: Springer, 2019: 122-144.
13	BOUDI Z, el KOURSI E M, COLLART-DUTILLEUL S. Colored Petri nets formal transformation to B machines for safety critical software development[C]//Proceedings of the International Conference on Industrial Engineering and Systems Management(IESM). Washington D. C., USA: IEEE Press, 2015: 12-18.
14	MORRIS K, SNOOK C, HOANG T S, et al. Formal verification and validation of Run-to-Completion style state charts using Event-B. Innovations in Systems and Software Engineering, 2022, 18 (4): 523- 541. doi: 10.1007/s11334-021-00416-4
15	MORRIS K, SNOOK C, HOANG T S, et al. Refinement and verification of responsive control systems[C]//Proceedings of International Conference on Rigorous State-Based Methods. Berlin, Germany: Springer, 2020: 272-277.
16	MORRIS K, SNOOK C, HOANG T S, et al. Refinement of statecharts with Run-to-Completion semantics[C]//Proceedings of International Workshop on Formal Techniques for Safety-Critical Systems. Berlin, Germany: Springer, 2019: 121-138.
17	ZOU L, ZHAN N J, WANG S L, et al. Formal verification of Simulink/Stateflow diagrams[C]//Proceedings of International Symposium on Automated Technology for Verification and Analysis. Berlin, Germany: Springer, 2015: 464-481.
18	BARNETT J. Introduction to SCXML[M]//DAHL D. Multimodal interaction with W3C standards. Berlin, Germany: Springer, 2017: 81-107.
19	KISTNER G, NUERNBERGER C. Developing user interfaces using SCXML statecharts[C]//Proceedings of the 1st Workshop on Engineering Interactive Computer Systems with SCXML. Washington D. C., USA: IEEE Press, 2014: 5-11.
20	SCHNELLE-WALKA D, RADECK-ARNETH S, STRIEBINGER J. Multimodal dialogmanagement in a smart home context with SCXML[C]//Proceedings of the 2nd Workshop on Engineering Interactive Computer Systems with SCXML. Washington D. C., USA: IEEE Press, 2015: 1-8.
21	MORRIS K, SNOOK C. Reconciling SCXML statechart representations and event-B lower level semantics[R]. Livermore, USA: Sandia National Lab., 2016: 1-5.
22	CLARKE E M, GRUMBERG O, HAMAGUCHI K. Another look at LTL model checking. Formal Methods in System Design, 1997, 10 (1): 47- 71. doi: 10.1023/A:1008615614281
23	HOARE C A R. Communicating sequential processes[M]. Englewood Cliffs, USA: Prentice/Hall International, 1985.
24	EZPELETA J, COUVREUR J M, SILVA M. A new technique for finding a generating family of siphons, traps and st-components. Application to colored Petri nets[M]//ROZENBERG G. Advances in Petri nets 1993. Berlin, Germany: Springer, 1993: 126-147.
25	ABRIAL J R, HOARE A. The B-book: assigning programs to meanings[M]. Cambridge, UK: Cambridge University Press, 1996.
26	BOULANGER J L. Formal methods applied to complex systems: implementation of the B Method. Computing Reviews, 2016, 57 (5): 267- 268. URL
27	LEUSCHEL M. ProB: harnessing the power of prolog to bring formal models and mathematics to life[M]//WARREN D S, DAHL V, EITER T, et al. Prolog: the next 50 years. Berlin, Germany: Springer, 2023: 239-247.
28	LECOMTE T. Teaching and training in formalisation with B[M]//DUBOIS C, SAN PIETRO P. Formal methods teaching. Berlin, Germany: Springer, 2023: 82-95.
29	VALMARI A. The state explosion problem[M]//REISIG W, ROZENBERG G. Lectures on Petri nets Ⅰ: basic models. Berlin, Germany: Springer, 1998: 429-528.
30	BEHM P, BENOIT P, FAIVRE A, et al. Météor: a successful application of B in a large project[C]//Proceedings of World Congress on Formal Methods in the Development of Computing Systems. Berlin, Germany: Springer, 1999: 369-387.
31	LECOMTE T, DEHARBE D, PRUN E, et al. Applying a formal method in industry: a 25-year trajectory[M]//CAVALHEIRO S, FIADEIRO J. Formal methods: foundations and applications. Berlin, Germany: Springer, 2017: 70-87.
32	CHIANG S H, MANSHARAMANI R K, VERNON M K. Use of application characteristics and limited preemption for Run-to-completion parallel processor scheduling policies. ACM SIGMETRICS Performance Evaluation Review, 1994, 22 (1): 33- 44. URL
33	MIAN Z, BOTTACI L, PAPADOPOULOS Y, et al. Model transformation for analyzing dependability of AADL model by using HiP-HOPS. Journal of Systems and Software, 2019, 151, 258- 282. doi: 10.1016/j.jss.2019.02.019
34	王恪铭, 王峥. 基于形式化方法的道口控制系统规范建模与验证. 西南交通大学学报, 2019, 54 (3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607
	WANG K M, WANG Z. Modeling and verification of control system specification for railway level crossings based on formal method. Journal of Southwest Jiaotong University, 2019, 54 (3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607

[1]	闫倩倩, 缪炜恺. 轨道交通控制软件中基于场景的需求分析方法[J]. 计算机工程, 2021, 47(8): 284-293,300.
[2]	杨锦翔, 熊焰, 黄文超. 基于强化学习的安全协议形式化验证优化研究[J]. 计算机工程, 2021, 47(12): 141-146.
[3]	陈金鑫,苏雯. 基于Event-B的自动化模块组合方法研究[J]. 计算机工程, 2019, 45(5): 298-307,314.
[4]	陈永,张薇,胡晓辉. 基于改进EventB建模的高速列车追踪运行仿真研究[J]. 计算机工程, 2015, 41(8): 256-261.
[5]	董昱, 水晶, 黎磊. CTCS-2级列控系统的形式化建模与验证[J]. 计算机工程, 2013, 39(3): 12-15.
[6]	徐亮，谭煌. BLP改进模型的形式化描述及自动化验证[J]. 计算机工程, 2013, 39(12): 130-135.
[7]	于淼, 李允, 桂盛霖, 罗蕾. 基于时间自动机的嵌入式系统调度分析工具[J]. 计算机工程, 2012, 38(3): 290-292.
[8]	马苏拉. 软件体系结构的广义视角研究[J]. 计算机工程, 2012, 38(23): 42-46.
[9]	周清雷, 张兵, 席琳. 基于模型检测的系统生存性分析[J]. 计算机工程, 2012, 38(17): 38-41.
[10]	赵硕, 陈中育, 肖春水. 基于范畴论的构件行为组合研究[J]. 计算机工程, 2012, 38(15): 53-55,58.
[11]	梁盟磊, 王小平, 薛小平, 李刚. 基于TLA的UML模型形式化验证[J]. 计算机工程, 2011, 37(2): 72-74.
[12]	陈兰香. 一种基于会话的安全Web文件服务模型[J]. 计算机工程, 2011, 37(18): 127-130.
[13]	陈振庆, 罗兰花. 基于动态描述逻辑的UML状态图形式化方法[J]. 计算机工程, 2011, 37(13): 55-57,60.
[14]	周绪川, 钟勇, 蔡利平. 机会发现在多智能体系统中的形式化描述方法[J]. 计算机工程, 2011, 37(11): 187-189.
[15]	郑斯琦;平玲娣;陈小平;顾文婷. 基于ISM的互操作性测试方法[J]. 计算机工程, 2010, 36(3): 72-75.

选择文件类型/文献管理软件名称

选择包含的内容