Basic Study on Formal Approaches to Systematic Development Methods of High-Quality Embedded Systems

我们在实际嵌入式系统的几个案例研究中构建了系统模型，并描述了它们的形式化规范。我们一直在使用正式的规范语言Z和VDM-SL（维也纳开发方法-规范语言）。在不同的抽象层次和系统开发的不同目的下，我们展示了描述和分析系统的有效方法。作为案例研究，我们建立了一个自动售货机的抽象模型，并展示了一种系统的方法将其增强为更高级和更复杂的模型。我们还从自动售货机的非正式和模糊的操作手册中导出了自动售货机控制器的正式描述。我们既用正式的规范语言描述了功能描述，又用Statecharts描述了其行为的动态描述。提出了一种从VDM-SL的形式化规范中导出状态图的系统方法，并提出了一种从形式化规范中导出状态图的系统方法。我们还开发了一个用于系统设计和分析中经常使用的图的通用分析工具。我们将其应用于各种问题，并展示了它的有用性，特别是在查询具有特定属性的受限路径时。我们研究了图分析器的扩展，以处理状态图和分析嵌入式系统的动态行为。

We constructed system models in several case studies of practical embedded systems in the real world, and described their formal specification. We have been using formal specification languages, Z and VDM-SL (Vienna Development Method - Specification Language). At different abstraction levels and different purposes in system development, we illustrated effective ways to describe and analyze the systems.As a case study, we made an abstract model for vending machines, and showed a systematic way to enhance it to more advanced and complicated models. We also derived a formal description for a controller of a vending machine from its informal and ambiguous operation manual. We described both a functional description in formal specification languages and a dynamic description of its behavior with Statecharts. We invented a systematic way to derive statecharts from a formal specification in VDM-SL, and then we proposed a systematic approach to get these two kinds of descriptions which are consistent and complementary each other.We also developed a generic analysis tool for diagrams which are used frequently in system design and analysis. We applied it to a variety of problems and showed its usefulness especially in querying constrained paths with specific attributes. We investigated the extension of the diagram analyzer to deal with Statecharts and analyze dynamic behaviors of embedded systems.