Object-oriented Development and Analysis of Embedded Systems

9901017 Betty cheng这个项目通过形式化统一建模语言（UML）的一部分，在嵌入式系统开发的正式和非正式方法之间架起了桥梁，UML是一种面向对象的建模符号，正在迅速成为事实上的标准。三种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.