Object-oriented Development and Analysis of Embedded Systems

9901017贝蒂·程这个项目通过将统一建模语言的一部分正式化，弥合了嵌入式系统开发的正式和非正式方法之间的差距。统一建模语言是一种面向对象的建模符号，正在迅速成为事实上的标准。本文将研究三种UML表示法、用例、类图和状态图；这三种模型足以代表嵌入式系统的需求。通过形式化，可以将模型集成到单个规范中，该规范可以分析一致性、并发属性(例如，死锁、活跃性)和约束满足情况。在选择表示法时，将评估如何使用模拟、模型检查以及这些方法的组合来分析它们。还将对这些规范进行评估，以确定它们在多大程度上可以用来构建自动设计转换，从而将图表细化为设计级规范。这些研究将产生一个框架，用于系统和严格地开发嵌入式系统，其中非正式需求被形式化，并利用设计信息进行细化，以获得相应的实现。将开发一个原型，以支持模型的图形化构造，生成相应的规范，并提供访问分析工具的途径。这些形式化将应用于日益复杂的案例研究，以确保该方法适用于来自行业的真实项目。

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.