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

我们在几个实际应用的嵌入式系统的案例研究中构建了系统模型，并描述了它们的形式化规范。我们一直在使用形式规范语言Z和VDM-SL(维也纳开发方法-规范语言)。在系统开发的不同抽象层次和不同目的下，阐述了对系统进行描述和分析的有效方法，并以自动售货机为例，建立了自动售货机的抽象模型，并展示了一种将其提升为更高级、更复杂模型的系统方法。我们还从非正式的、模棱两可的操作手册中推导出自动售货机控制器的形式化描述。我们既用形式规范语言描述了函数描述，又用状态图描述了其行为的动态描述。提出了一种系统地从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.