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 Chengths项目通过正式化统一建模语言（UML）的一部分，这是一种面向对象的建模符号，从而迅速成为事实上的标准，从而弥合了正式和非正式方法之间嵌入式系统开发的差距。 将研究三个UML符号，用例，类图和状态图；这三个模型充分表示嵌入式系统的要求。 通过形式化，可以将模型集成到单个规范中，该规范可以进行分析以确保一致性，并发属性（例如，僵局，livices）和约束满意度。 在选择表示形式时，将对如何使用模拟，模型检查以及这些方法的组合进行评估。 还将评估规格，以确定它们如何用于构建自动化设计转换，以将图完善到设计级别的规格中。 调查将为系统和严格开发的系统产生一个框架，在该系统中，非正式要求是正式的，并使用设计信息进行了完善，以获得相应的实施。 将开发一个原型，以支持模型的图形结构，生成相应的规格并提供对分析工具的访问。 形式化将应用于日益复杂的案例研究，以确保该方法适用于行业的实际项目。