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

摘要：近年来，分布式实时嵌入式系统（DREs）的需求和复杂性显著增加，应用于汽车、航空航天、制造业、医疗系统和电信等许多领域。DREs数量和复杂性的增加强烈地激发了对更严格的、可重复的和经济有效的开发技术的需求。为了应对这一挑战，我们建议开发一些技术和工件，这些技术和工件将促进DREs的建模和分析，目的是在设计、编码和制造之前的早期开发阶段预防和/或检测错误。具体来说，我们将开发UML的扩展，以表示适用于DREs的时间信息；为DRE开发对象分析模式，包括带有DRE扩展的UML图模板；并开发基于时间的正式规范模式，以指定DREs的关键安全特性。这个项目更广泛的影响是，通过将非正式的、常用的技术与严格的、更正式的技术连接起来，一个更大的开发社区能够构建更高质量的模型和DRE系统。例如，将为正式规范开发自然语言前端，以使更广泛的DRE开发社区更容易访问正式规范模式。为了自动分析UML图，我们将扩展我们以前开发的UML形式化框架，从具有DRE扩展的UML图中自动生成相应的形式化规范。然后可以通过模拟或模型检查来分析这些规范是否符合关键属性（用规范模式指定）。根据原始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.