Combining SysML with Petri Nets for the Design of an Urban Traffic Signal Control

Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application

Building SysML Model Graph to Support the System Model Reuse

顶刊：

  • (A)Baresi L, Morzenti A, Motta A, et al. A logic-based approach for the verification of UML timed models[J]. ACM Transactions on Software Engineering and Methodology (TOSEM). 2017, 26(2):7.

    在 UML/MARTE 的基础上提出了一种名为 C-UML 的建模语言。该语言允许使用多种视图对嵌入式实时系统的组件及行为进行建模，但是其语义还需要进一步完善。

  • (B) Ribeiro F G C, Pereira C E, Rettberg A, et al. Model-based requirements specification of real-time systems with UML, SysML and MARTE[J]. Software & Systems Modeling. 2018, 17(1):343–361

    探讨了如何将 UML 与 SysML和 MARTE 进行结合，以便用于实时系统的时间、行为和软硬件需求的建模，不足的是多个语言之间的协作运用增加了该方法在应用时的难度。

  • (B) Yu H, Ma Y, Gautier T, et al. Polychronous modeling, analysis, verification and simulation for timed software architectures[J]. Journal of Systems Architecture.2013, 59(10):1157–1170.

    描述了一种有效可行的方法用于时间软件体系架构的建模、验证和仿真。该方法以Simulink 工具为基础，能够通过一个多时钟计算模型，对整个系统的时延进行分析和验证。

  • Märtin L, Schatalov M, Hagner M, et al. A methodology for model-based development and automated verification of software for aerospace systems[C]. 2013 IEEE aerospace conference. New York: IEEE, 2013: 1–19.

    提出一种面向航空航天系统软件的模型驱动开发方法，该方法使用了 SCADE 工具来支持关键性能的自动验证和分析。

其他

  • 从Lustre到Simulink

From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications.

介绍了从Lustre模型到真正的MatlabSimulink的编译过程，无需依赖外部C函数或MATLAB函数。此转换基于Lustre到命令式代码的模块化编译，并在生成的Simulink模型中保留输入Lustre模型的层次结构。我们实现了该方法，并使用它来验证编译工具链，通过等价性测试和检查，将Simulink映射到Lustre，然后映射到C。从Lustre到Simulink的这种向后编译还提供了自动生成Simulink组件建模规范、证明参数或测试用例覆盖率标准的能力。

Integrating SysML with Simulation Environments (Simulink) by Model Transformation Approach

在系统级设计中，描述性系统模型似乎不足以执行满足各种利益相关者需求的系统验证。这一事实由于系统工程项目日益复杂而更加突出，因此，难以处理它们的协调和可追溯性。即使SysML（系统建模语言）被认为是系统工程的一种灵活的标准工具，仅使用描述性模型也不足以进行系统行为验证。为了解决这一问题，仿真环境（即MATLAB/Simulink）允许验证系统初步设计是否满足要求。因此，各种研究工作都集中在结合SysML建模和仿真工具的潜力上。本文提出了一种基于元建模和模型转换的集成方法，从SysML图生成Simulink模型。这种方法由模型和MDE（模型驱动工程）的现代技术处理。

  • A logic-based approach for the verification of UML timed models[J]. ACM Transactions on Software Engineering and Methodology (TOSEM). 2017, 26(2):7.

  • Model-based requirements specification of real-time systems with UML, SysML and MARTE[J]. Software & Systems Modeling. 2018, 17(1):343–361

  • Polychronous modeling, analysis, verification and simulation for timed software architectures[J]. Journal of Systems Architecture.2013, 59(10):1157–1170.

  • A methodology for model-based development and automated verification of software for aerospace systems[C]. 2013 IEEE aerospace conference. New York: IEEE, 2013: 1–19.

  • Convergence of physical system and cyber system modeling methods for aviation cyber physical control system,” in 2014 IEEE International Conference on Information and Automation (ICIA). IEEE, 2014, pp. 542–547.

  • Modeling of communication-based train control (cbtc) radio channel with leaky waveguide” IEEE Antennas and Wireless Propagation Letters, vol. 12, pp. 1061–1064, 2013.

  • A Declarative Approach for Transforming SysML Models to Executable Simulation Models. IEEE Trans. Syst. Man Cybern. Syst. 51(6): 3330-3345 (2021)

  • Model-Based Design of Correct Safety-Critical Systems using Dataflow Languages on the Example of SysML Architecture and Behavior Diagrams. Software Engineering (Satellite Events) 2021

  • Survey of model-based systems engineering (mbse) methodologies,” Incose MBSE Focus Group, vol. 25, no. 8, pp. 1–12, 2007.

  • The Kind 2 Model Checker. In: Chaudhuri S., Farzan A. (eds) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science, vol 9780. Springer, Cham.

  • Composing Hierarchical Stochastic Model from SysML for System Availability Analysis

  • Describing Software Specification by Combining SysML with the B method

  • Successive Refinement of Models for Model-Based Testing to Increase System Test Effectiveness

  • Verifying the safety of a flflight-critical system. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308–324. Springer, Heidelberg (2015)

  • Formal verifification and validation of embedded systems: the UML-based MADES approach. Software and Systems Modeling 14, 1 (2015), 343–363.

  • TURTLE: a real-time UML profifile supported by a formal validation toolkit. IEEE Transactions on Software Engineering 30, 7 (2004), 473–487

  • A Logic-based Semantics for the Verifification of Multi-diagram UML Models. SIGSOFT Softw. Eng. Notes 37, 4 (July 2012), 1–8.

  • “Model-checking of safety-critical software for avionics.” ERCIM News 75 (2008): 15-16.

  • Combining SysML with Petri Nets for the Design of an Urban Traffic Signal Control. ICCSA (9) 2021: 115-126