Object-oriented Development and Analysis of Embedded Systems

嵌入式系统的面向对象开发与分析

• 批准号: 9901017
• 负责人: Betty Cheng
• 金额: $ 36.5万
• 依托单位: Michigan State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-08-15 至 2006-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9901017&HistoricalAwards=false
• 关键词: Object; oriented; Development; Analysis; Embedded

9901017 Betty ChengThis project bridges the gap between formal and informal approaches to embedded systems development by formalizing part of the Unified Modeling Language (UML), an object-oriented modeling notation that is quickly becoming the de facto standard. Three of the UML notations, use cases, class diagrams, and state diagrams will be investigated; these three models sufficiently represent embedded-systems requirements. Through formalization, the models can be integrated into a single specification that can be analyzed for consistency, concurrency properties (e.g., deadlock, liveness), and constraint satisfaction. In choosing the representations, an assessment will be made as to how they can be analyzed using simulation, model checking, and a combination of these approaches. The specifications will also be assessed to determine how well they can be used to construct automated design transformations that refine the diagrams into design-level specifications. The investigations will yield a framework for systematically and rigorously developingembedded systems, where informal requirements are formalized and refined with design information to obtain the corresponding implementation. A prototype will be developed to support the graphical construction of the models, generate the corresponding specifications, and provide access to the analysis tools. The formalizations will be applied to increasingly complex case studies to ensure that the approach is applicable to real projects from industry.

9901017 Betty Cheng该项目通过形式化统一建模语言（UML）的一部分，弥合了嵌入式系统开发的正式和非正式方法之间的差距，UML是一种面向对象的建模符号，正在迅速成为事实上的标准。 我们将研究三种UML符号，用例、类图和状态图;这三种模型充分地表示了嵌入式系统的需求。 通过形式化，可以将模型集成到单个规范中，可以分析该规范的一致性、并发属性（例如，死锁、活跃度）和约束满足。 在选择的表示，将作出评估，以如何可以使用模拟，模型检查，以及这些方法的组合进行分析。 规范也将被评估，以确定如何使用它们来构建自动化设计转换，将图细化为设计级规范。 这些调查将产生一个框架，系统和严格的developingembedded系统，非正式的要求是正式的和完善的设计信息，以获得相应的实施。 将开发一个原型，以支持模型的图形构建，生成相应的规格，并提供分析工具。 形式化将被应用到越来越复杂的案例研究，以确保该方法适用于真实的项目，从行业。