Facilitating the Modeling and Analysis of Distributed Real-time Embedded Systems

标题：促进分布式实时嵌入式系统的建模和分析近年来，分布式实时嵌入式系统(DRE)的需求和复杂性显著增加，出现在许多应用中，例如汽车、航空航天、制造、医疗系统和电信。DRE数量和复杂性的增加强烈推动了对更严格、可重复和成本效益更高的开发技术的需求。为了应对这一挑战，我们建议开发一些技术和人工制品，以促进DRE的建模和分析，目的是在设计、编码和制造之前的开发早期阶段防止和/或检测错误。具体地说，我们将开发对UML的扩展，以表示适用于DRE的计时信息；为DRE开发对象分析模式，包括具有DRE扩展的UML图的模板；以及开发基于计时的形式规范模式，用于指定DRE的关键安全属性。这个项目的更广泛的影响是，通过将非正式的、常用的技术与严格的、更正式的技术相结合，更大的开发社区能够构建更高质量的模型和DRE系统。例如，将为正式规范开发自然语言前端，以使更广泛的DRE开发社区更容易访问正式规范模式。为了自动分析UML图，我们将扩展我们之前开发的UML形式化框架，以自动从带有DRE扩展的UML图中生成相应的形式化规范。然后可以通过模拟或模型检查这些规范是否符合关键属性(由规范模式指定)来分析这些规范。分析错误将根据原始的UML图进行可视化，从而促进了创建和改进UML模型的往返工程方法。统一建模语言和形式化规范模式都将基于对从行业合作伙伴获得的项目的分析而开发，从而进一步确保了对行业项目的实用性和适用性。

ABSTRACT0541131Betty ChengMichigan State UniversityTitle: Facilitating the Modeling and Analysis of Distributed Real-time Embedded Systems The demand for and complexity of distributed real-time embedded systems (DREs) has increased considerably in recent years, occurring in many applications, such as automotive, aerospace, manufacturing, medical systems, and telecommunication. The increase in the number and complexity of DREs strongly motivates the need for more rigorous, repeatable, and cost-effective development techniques. To address this challenge, we propose to develop a number of techniques and artifacts that will facilitate the modeling and analysis of DREs, with the intent of preventing and/or detecting errors in the early stages of development prior to design, coding, and fabrication. Specifically, we will develop extensions to UML to denote timing information applicable to DREs; develop object analysis patterns for DREs comprising templates for UML diagrams with DRE extensions; and develop timing-based formal specification patterns for specifying critical safety properties of DREs. The broader impact of this project is that by bridging informal, commonly-used techniques with rigorous, and more formal techniques, a larger development community is able to build higher quality models and DRE systems. For example, a natural-language front-end will be developed for the formal specifications to make the formal specification patterns more accessible to the broader DRE development community. In order to automatically analyze the UML diagrams, we will extend our previously developed UML formalization framework to automatically generate corresponding formal specifications from the UML diagrams with DRE extensions. These specification can then be analyzed by simulation or model checked for adherence to criticalproperties (specified with the specification patterns). Analysis errors will be visualized in terms of the original UML diagrams, thus facilitating a round-trip engineering approach to UML model creation and refinement. Both the UML and the formal specification patterns will developed based on analyses of projects obtained from industrial partners, thus further ensuring the utility and applicability to industrial projects.